 Home Intuitionistic Logic ExplorerTheorem List (p. 56 of 95) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 5501-5600   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremoprabbidv 5501* Equivalent wff's yield equal operation class abstractions (deduction rule). (Contributed by NM, 21-Feb-2004.)
(φ → (ψχ))       (φ → {⟨⟨x, y⟩, z⟩ ∣ ψ} = {⟨⟨x, y⟩, z⟩ ∣ χ})

Theoremoprabbii 5502* Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
(φψ)       {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, z⟩ ∣ ψ}

Theoremssoprab2 5503 Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 4003. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
(xyz(φψ) → {⟨⟨x, y⟩, z⟩ ∣ φ} ⊆ {⟨⟨x, y⟩, z⟩ ∣ ψ})

Theoremssoprab2b 5504 Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b 4004. (Contributed by FL, 6-Nov-2013.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
({⟨⟨x, y⟩, z⟩ ∣ φ} ⊆ {⟨⟨x, y⟩, z⟩ ∣ ψ} ↔ xyz(φψ))

Theoremeqoprab2b 5505 Equivalence of ordered pair abstraction subclass and biconditional. Compare eqopab2b 4007. (Contributed by Mario Carneiro, 4-Jan-2017.)
({⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, z⟩ ∣ ψ} ↔ xyz(φψ))

Theoremmpt2eq123 5506* An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
((A = 𝐷 x A (B = 𝐸 y B 𝐶 = 𝐹)) → (x A, y B𝐶) = (x 𝐷, y 𝐸𝐹))

Theoremmpt2eq12 5507* An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
((A = 𝐶 B = 𝐷) → (x A, y B𝐸) = (x 𝐶, y 𝐷𝐸))

Theoremmpt2eq123dva 5508* An equality deduction for the maps to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
(φA = 𝐷)    &   ((φ x A) → B = 𝐸)    &   ((φ (x A y B)) → 𝐶 = 𝐹)       (φ → (x A, y B𝐶) = (x 𝐷, y 𝐸𝐹))

Theoremmpt2eq123dv 5509* An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.)
(φA = 𝐷)    &   (φB = 𝐸)    &   (φ𝐶 = 𝐹)       (φ → (x A, y B𝐶) = (x 𝐷, y 𝐸𝐹))

Theoremmpt2eq123i 5510 An equality inference for the maps to notation. (Contributed by NM, 15-Jul-2013.)
A = 𝐷    &   B = 𝐸    &   𝐶 = 𝐹       (x A, y B𝐶) = (x 𝐷, y 𝐸𝐹)

Theoremmpt2eq3dva 5511* Slightly more general equality inference for the maps to notation. (Contributed by NM, 17-Oct-2013.)
((φ x A y B) → 𝐶 = 𝐷)       (φ → (x A, y B𝐶) = (x A, y B𝐷))

Theoremmpt2eq3ia 5512 An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
((x A y B) → 𝐶 = 𝐷)       (x A, y B𝐶) = (x A, y B𝐷)

Theoremnfmpt21 5513 Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
x(x A, y B𝐶)

Theoremnfmpt22 5514 Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
y(x A, y B𝐶)

Theoremnfmpt2 5515* Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
zA    &   zB    &   z𝐶       z(x A, y B𝐶)

Theoremmpt20 5516 A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
(x ∅, y B𝐶) = ∅

Theoremoprab4 5517* Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010.)
{⟨⟨x, y⟩, z⟩ ∣ (⟨x, y (A × B) φ)} = {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) φ)}

Theoremcbvoprab1 5518* Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008.) (Revised by Mario Carneiro, 5-Dec-2016.)
wφ    &   xψ    &   (x = w → (φψ))       {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨w, y⟩, z⟩ ∣ ψ}

Theoremcbvoprab2 5519* Change the second bound variable in an operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)
wφ    &   yψ    &   (y = w → (φψ))       {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, w⟩, z⟩ ∣ ψ}

Theoremcbvoprab12 5520* Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
wφ    &   vφ    &   xψ    &   yψ    &   ((x = w y = v) → (φψ))       {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨w, v⟩, z⟩ ∣ ψ}

Theoremcbvoprab12v 5521* Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.)
((x = w y = v) → (φψ))       {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨w, v⟩, z⟩ ∣ ψ}

Theoremcbvoprab3 5522* Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013.)
wφ    &   zψ    &   (z = w → (φψ))       {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, w⟩ ∣ ψ}

Theoremcbvoprab3v 5523* Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004.) (Revised by David Abernethy, 19-Jun-2012.)
(z = w → (φψ))       {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨⟨x, y⟩, w⟩ ∣ ψ}

Theoremcbvmpt2x 5524* Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 5525 allows B to be a function of x. (Contributed by NM, 29-Dec-2014.)
zB    &   x𝐷    &   z𝐶    &   w𝐶    &   x𝐸    &   y𝐸    &   (x = zB = 𝐷)    &   ((x = z y = w) → 𝐶 = 𝐸)       (x A, y B𝐶) = (z A, w 𝐷𝐸)

Theoremcbvmpt2 5525* Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.)
z𝐶    &   w𝐶    &   x𝐷    &   y𝐷    &   ((x = z y = w) → 𝐶 = 𝐷)       (x A, y B𝐶) = (z A, w B𝐷)

Theoremcbvmpt2v 5526* Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 3842, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)
(x = z𝐶 = 𝐸)    &   (y = w𝐸 = 𝐷)       (x A, y B𝐶) = (z A, w B𝐷)

Theoremdmoprab 5527* The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995.) (Revised by David Abernethy, 19-Jun-2012.)
dom {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨x, y⟩ ∣ zφ}

Theoremdmoprabss 5528* The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995.)
dom {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) φ)} ⊆ (A × B)

Theoremrnoprab 5529* The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004.) (Revised by David Abernethy, 19-Apr-2013.)
ran {⟨⟨x, y⟩, z⟩ ∣ φ} = {zxyφ}

Theoremrnoprab2 5530* The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012.)
ran {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) φ)} = {zx A y B φ}

Theoremreldmoprab 5531* The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995.)
Rel dom {⟨⟨x, y⟩, z⟩ ∣ φ}

Theoremoprabss 5532* Structure of an operation class abstraction. (Contributed by NM, 28-Nov-2006.)
{⟨⟨x, y⟩, z⟩ ∣ φ} ⊆ ((V × V) × V)

Theoremeloprabga 5533* The law of concretion for operation class abstraction. Compare elopab 3986. (Contributed by NM, 14-Sep-1999.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.)
((x = A y = B z = 𝐶) → (φψ))       ((A 𝑉 B 𝑊 𝐶 𝑋) → (⟨⟨A, B⟩, 𝐶 {⟨⟨x, y⟩, z⟩ ∣ φ} ↔ ψ))

Theoremeloprabg 5534* The law of concretion for operation class abstraction. Compare elopab 3986. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)
(x = A → (φψ))    &   (y = B → (ψχ))    &   (z = 𝐶 → (χθ))       ((A 𝑉 B 𝑊 𝐶 𝑋) → (⟨⟨A, B⟩, 𝐶 {⟨⟨x, y⟩, z⟩ ∣ φ} ↔ θ))

Theoremssoprab2i 5535* Inference of operation class abstraction subclass from implication. (Contributed by NM, 11-Nov-1995.) (Revised by David Abernethy, 19-Jun-2012.)
(φψ)       {⟨⟨x, y⟩, z⟩ ∣ φ} ⊆ {⟨⟨x, y⟩, z⟩ ∣ ψ}

Theoremmpt2v 5536* Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
(x V, y V ↦ 𝐶) = {⟨⟨x, y⟩, z⟩ ∣ z = 𝐶}

Theoremmpt2mptx 5537* Express a two-argument function as a one-argument function, or vice-versa. In this version B(x) is not assumed to be constant w.r.t x. (Contributed by Mario Carneiro, 29-Dec-2014.)
(z = ⟨x, y⟩ → 𝐶 = 𝐷)       (z x A ({x} × B) ↦ 𝐶) = (x A, y B𝐷)

Theoremmpt2mpt 5538* Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by Mario Carneiro, 29-Dec-2014.)
(z = ⟨x, y⟩ → 𝐶 = 𝐷)       (z (A × B) ↦ 𝐶) = (x A, y B𝐷)

Theoremresoprab 5539* Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007.)
({⟨⟨x, y⟩, z⟩ ∣ φ} ↾ (A × B)) = {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) φ)}

Theoremresoprab2 5540* Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
((𝐶A 𝐷B) → ({⟨⟨x, y⟩, z⟩ ∣ ((x A y B) φ)} ↾ (𝐶 × 𝐷)) = {⟨⟨x, y⟩, z⟩ ∣ ((x 𝐶 y 𝐷) φ)})

Theoremresmpt2 5541* Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)
((𝐶A 𝐷B) → ((x A, y B𝐸) ↾ (𝐶 × 𝐷)) = (x 𝐶, y 𝐷𝐸))

Theoremfunoprabg 5542* "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 28-Aug-2007.)
(xy∃*zφ → Fun {⟨⟨x, y⟩, z⟩ ∣ φ})

Theoremfunoprab 5543* "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 17-Mar-1995.)
∃*zφ       Fun {⟨⟨x, y⟩, z⟩ ∣ φ}

Theoremfnoprabg 5544* Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007.)
(xy(φ∃!zψ) → {⟨⟨x, y⟩, z⟩ ∣ (φ ψ)} Fn {⟨x, y⟩ ∣ φ})

Theoremmpt2fun 5545* The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.)
𝐹 = (x A, y B𝐶)       Fun 𝐹

Theoremfnoprab 5546* Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995.)
(φ∃!zψ)       {⟨⟨x, y⟩, z⟩ ∣ (φ ψ)} Fn {⟨x, y⟩ ∣ φ}

Theoremffnov 5547* An operation maps to a class to which all values belong. (Contributed by NM, 7-Feb-2004.)
(𝐹:(A × B)⟶𝐶 ↔ (𝐹 Fn (A × B) x A y B (x𝐹y) 𝐶))

Theoremfovcl 5548 Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
𝐹:(𝑅 × 𝑆)⟶𝐶       ((A 𝑅 B 𝑆) → (A𝐹B) 𝐶)

Theoremeqfnov 5549* Equality of two operations is determined by their values. (Contributed by NM, 1-Sep-2005.)
((𝐹 Fn (A × B) 𝐺 Fn (𝐶 × 𝐷)) → (𝐹 = 𝐺 ↔ ((A × B) = (𝐶 × 𝐷) x A y B (x𝐹y) = (x𝐺y))))

Theoremeqfnov2 5550* Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010.)
((𝐹 Fn (A × B) 𝐺 Fn (A × B)) → (𝐹 = 𝐺x A y B (x𝐹y) = (x𝐺y)))

Theoremfnovim 5551* Representation of a function in terms of its values. (Contributed by Jim Kingdon, 16-Jan-2019.)
(𝐹 Fn (A × B) → 𝐹 = (x A, y B ↦ (x𝐹y)))

Theoremmpt22eqb 5552* Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 5550. (Contributed by Mario Carneiro, 4-Jan-2017.)
(x A y B 𝐶 𝑉 → ((x A, y B𝐶) = (x A, y B𝐷) ↔ x A y B 𝐶 = 𝐷))

Theoremrnmpt2 5553* The range of an operation given by the "maps to" notation. (Contributed by FL, 20-Jun-2011.)
𝐹 = (x A, y B𝐶)       ran 𝐹 = {zx A y B z = 𝐶}

Theoremreldmmpt2 5554* The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.)
𝐹 = (x A, y B𝐶)       Rel dom 𝐹

Theoremelrnmpt2g 5555* Membership in the range of an operation class abstraction. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
𝐹 = (x A, y B𝐶)       (𝐷 𝑉 → (𝐷 ran 𝐹x A y B 𝐷 = 𝐶))

Theoremelrnmpt2 5556* Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
𝐹 = (x A, y B𝐶)    &   𝐶 V       (𝐷 ran 𝐹x A y B 𝐷 = 𝐶)

Theoremralrnmpt2 5557* A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)
𝐹 = (x A, y B𝐶)    &   (z = 𝐶 → (φψ))       (x A y B 𝐶 𝑉 → (z ran 𝐹φx A y B ψ))

Theoremrexrnmpt2 5558* A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)
𝐹 = (x A, y B𝐶)    &   (z = 𝐶 → (φψ))       (x A y B 𝐶 𝑉 → (z ran 𝐹φx A y B ψ))

Theoremovid 5559* The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
((x 𝑅 y 𝑆) → ∃!zφ)    &   𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x 𝑅 y 𝑆) φ)}       ((x 𝑅 y 𝑆) → ((x𝐹y) = zφ))

Theoremovidig 5560* The value of an operation class abstraction. Compare ovidi 5561. The condition (x 𝑅 y 𝑆) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.)
∃*zφ    &   𝐹 = {⟨⟨x, y⟩, z⟩ ∣ φ}       (φ → (x𝐹y) = z)

Theoremovidi 5561* The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014.)
((x 𝑅 y 𝑆) → ∃*zφ)    &   𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x 𝑅 y 𝑆) φ)}       ((x 𝑅 y 𝑆) → (φ → (x𝐹y) = z))

Theoremov 5562* The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
𝐶 V    &   (x = A → (φψ))    &   (y = B → (ψχ))    &   (z = 𝐶 → (χθ))    &   ((x 𝑅 y 𝑆) → ∃!zφ)    &   𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x 𝑅 y 𝑆) φ)}       ((A 𝑅 B 𝑆) → ((A𝐹B) = 𝐶θ))

Theoremovigg 5563* The value of an operation class abstraction. Compare ovig 5564. The condition (x 𝑅 y 𝑆) is been removed. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)
((x = A y = B z = 𝐶) → (φψ))    &   ∃*zφ    &   𝐹 = {⟨⟨x, y⟩, z⟩ ∣ φ}       ((A 𝑉 B 𝑊 𝐶 𝑋) → (ψ → (A𝐹B) = 𝐶))

Theoremovig 5564* The value of an operation class abstraction (weak version). (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 14-Sep-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
((x = A y = B z = 𝐶) → (φψ))    &   ((x 𝑅 y 𝑆) → ∃*zφ)    &   𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x 𝑅 y 𝑆) φ)}       ((A 𝑅 B 𝑆 𝐶 𝐷) → (ψ → (A𝐹B) = 𝐶))

Theoremovmpt4g 5565* Value of a function given by the "maps to" notation. (This is the operation analog of fvmpt2 5197.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)
𝐹 = (x A, y B𝐶)       ((x A y B 𝐶 𝑉) → (x𝐹y) = 𝐶)

Theoremovmpt2s 5566* Value of a function given by the "maps to" notation, expressed using explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.)
𝐹 = (x 𝐶, y 𝐷𝑅)       ((A 𝐶 B 𝐷 A / xB / y𝑅 𝑉) → (A𝐹B) = A / xB / y𝑅)

Theoremov2gf 5567* The value of an operation class abstraction. A version of ovmpt2g 5577 using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 19-Dec-2013.)
xA    &   yA    &   yB    &   x𝐺    &   y𝑆    &   (x = A𝑅 = 𝐺)    &   (y = B𝐺 = 𝑆)    &   𝐹 = (x 𝐶, y 𝐷𝑅)       ((A 𝐶 B 𝐷 𝑆 𝐻) → (A𝐹B) = 𝑆)

Theoremovmpt2dxf 5568* Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
(φ𝐹 = (x 𝐶, y 𝐷𝑅))    &   ((φ (x = A y = B)) → 𝑅 = 𝑆)    &   ((φ x = A) → 𝐷 = 𝐿)    &   (φA 𝐶)    &   (φB 𝐿)    &   (φ𝑆 𝑋)    &   xφ    &   yφ    &   yA    &   xB    &   x𝑆    &   y𝑆       (φ → (A𝐹B) = 𝑆)

Theoremovmpt2dx 5569* Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
(φ𝐹 = (x 𝐶, y 𝐷𝑅))    &   ((φ (x = A y = B)) → 𝑅 = 𝑆)    &   ((φ x = A) → 𝐷 = 𝐿)    &   (φA 𝐶)    &   (φB 𝐿)    &   (φ𝑆 𝑋)       (φ → (A𝐹B) = 𝑆)

Theoremovmpt2d 5570* Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014.)
(φ𝐹 = (x 𝐶, y 𝐷𝑅))    &   ((φ (x = A y = B)) → 𝑅 = 𝑆)    &   (φA 𝐶)    &   (φB 𝐷)    &   (φ𝑆 𝑋)       (φ → (A𝐹B) = 𝑆)

Theoremovmpt2x 5571* The value of an operation class abstraction. Variant of ovmpt2ga 5572 which does not require 𝐷 and x to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
((x = A y = B) → 𝑅 = 𝑆)    &   (x = A𝐷 = 𝐿)    &   𝐹 = (x 𝐶, y 𝐷𝑅)       ((A 𝐶 B 𝐿 𝑆 𝐻) → (A𝐹B) = 𝑆)

Theoremovmpt2ga 5572* Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.)
((x = A y = B) → 𝑅 = 𝑆)    &   𝐹 = (x 𝐶, y 𝐷𝑅)       ((A 𝐶 B 𝐷 𝑆 𝐻) → (A𝐹B) = 𝑆)

Theoremovmpt2a 5573* Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.)
((x = A y = B) → 𝑅 = 𝑆)    &   𝐹 = (x 𝐶, y 𝐷𝑅)    &   𝑆 V       ((A 𝐶 B 𝐷) → (A𝐹B) = 𝑆)

Theoremovmpt2df 5574* Alternate deduction version of ovmpt2 5578, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
(φA 𝐶)    &   ((φ x = A) → B 𝐷)    &   ((φ (x = A y = B)) → 𝑅 𝑉)    &   ((φ (x = A y = B)) → ((A𝐹B) = 𝑅ψ))    &   x𝐹    &   xψ    &   y𝐹    &   yψ       (φ → (𝐹 = (x 𝐶, y 𝐷𝑅) → ψ))

Theoremovmpt2dv 5575* Alternate deduction version of ovmpt2 5578, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
(φA 𝐶)    &   ((φ x = A) → B 𝐷)    &   ((φ (x = A y = B)) → 𝑅 𝑉)    &   ((φ (x = A y = B)) → ((A𝐹B) = 𝑅ψ))       (φ → (𝐹 = (x 𝐶, y 𝐷𝑅) → ψ))

Theoremovmpt2dv2 5576* Alternate deduction version of ovmpt2 5578, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
(φA 𝐶)    &   ((φ x = A) → B 𝐷)    &   ((φ (x = A y = B)) → 𝑅 𝑉)    &   ((φ (x = A y = B)) → 𝑅 = 𝑆)       (φ → (𝐹 = (x 𝐶, y 𝐷𝑅) → (A𝐹B) = 𝑆))

Theoremovmpt2g 5577* Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)
(x = A𝑅 = 𝐺)    &   (y = B𝐺 = 𝑆)    &   𝐹 = (x 𝐶, y 𝐷𝑅)       ((A 𝐶 B 𝐷 𝑆 𝐻) → (A𝐹B) = 𝑆)

Theoremovmpt2 5578* Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
(x = A𝑅 = 𝐺)    &   (y = B𝐺 = 𝑆)    &   𝐹 = (x 𝐶, y 𝐷𝑅)    &   𝑆 V       ((A 𝐶 B 𝐷) → (A𝐹B) = 𝑆)

Theoremovi3 5579* The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)
(((A 𝐻 B 𝐻) (𝐶 𝐻 𝐷 𝐻)) → 𝑆 (𝐻 × 𝐻))    &   (((w = A v = B) (u = 𝐶 f = 𝐷)) → 𝑅 = 𝑆)    &   𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x (𝐻 × 𝐻) y (𝐻 × 𝐻)) wvuf((x = ⟨w, v y = ⟨u, f⟩) z = 𝑅))}       (((A 𝐻 B 𝐻) (𝐶 𝐻 𝐷 𝐻)) → (⟨A, B𝐹𝐶, 𝐷⟩) = 𝑆)

Theoremov6g 5580* The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006.)
(⟨x, y⟩ = ⟨A, B⟩ → 𝑅 = 𝑆)    &   𝐹 = {⟨⟨x, y⟩, z⟩ ∣ (⟨x, y 𝐶 z = 𝑅)}       (((A 𝐺 B 𝐻 A, B 𝐶) 𝑆 𝐽) → (A𝐹B) = 𝑆)

Theoremovg 5581* The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
(x = A → (φψ))    &   (y = B → (ψχ))    &   (z = 𝐶 → (χθ))    &   ((τ (x 𝑅 y 𝑆)) → ∃!zφ)    &   𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ((x 𝑅 y 𝑆) φ)}       ((τ (A 𝑅 B 𝑆 𝐶 𝐷)) → ((A𝐹B) = 𝐶θ))

Theoremovres 5582 The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
((A 𝐶 B 𝐷) → (A(𝐹 ↾ (𝐶 × 𝐷))B) = (A𝐹B))

Theoremovresd 5583 Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
(φA 𝑋)    &   (φB 𝑋)       (φ → (A(𝐷 ↾ (𝑋 × 𝑋))B) = (A𝐷B))

Theoremoprssov 5584 The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007.)
(((Fun 𝐹 𝐺 Fn (𝐶 × 𝐷) 𝐺𝐹) (A 𝐶 B 𝐷)) → (A𝐹B) = (A𝐺B))

Theoremfovrn 5585 An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.)
((𝐹:(𝑅 × 𝑆)⟶𝐶 A 𝑅 B 𝑆) → (A𝐹B) 𝐶)

Theoremfovrnda 5586 An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
(φ𝐹:(𝑅 × 𝑆)⟶𝐶)       ((φ (A 𝑅 B 𝑆)) → (A𝐹B) 𝐶)

Theoremfovrnd 5587 An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
(φ𝐹:(𝑅 × 𝑆)⟶𝐶)    &   (φA 𝑅)    &   (φB 𝑆)       (φ → (A𝐹B) 𝐶)

Theoremfnrnov 5588* The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006.)
(𝐹 Fn (A × B) → ran 𝐹 = {zx A y B z = (x𝐹y)})

Theoremfoov 5589* An onto mapping of an operation expressed in terms of operation values. (Contributed by NM, 29-Oct-2006.)
(𝐹:(A × B)–onto𝐶 ↔ (𝐹:(A × B)⟶𝐶 z 𝐶 x A y B z = (x𝐹y)))

Theoremfnovrn 5590 An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007.)
((𝐹 Fn (A × B) 𝐶 A 𝐷 B) → (𝐶𝐹𝐷) ran 𝐹)

Theoremovelrn 5591* A member of an operation's range is a value of the operation. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
(𝐹 Fn (A × B) → (𝐶 ran 𝐹x A y B 𝐶 = (x𝐹y)))

Theoremfunimassov 5592* Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
((Fun 𝐹 (A × B) ⊆ dom 𝐹) → ((𝐹 “ (A × B)) ⊆ 𝐶x A y B (x𝐹y) 𝐶))

Theoremovelimab 5593* Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
((𝐹 Fn A (B × 𝐶) ⊆ A) → (𝐷 (𝐹 “ (B × 𝐶)) ↔ x B y 𝐶 𝐷 = (x𝐹y)))

Theoremovconst2 5594 The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
𝐶 V       ((𝑅 A 𝑆 B) → (𝑅((A × B) × {𝐶})𝑆) = 𝐶)

Theoremcaovclg 5595* Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.)
((φ (x 𝐶 y 𝐷)) → (x𝐹y) 𝐸)       ((φ (A 𝐶 B 𝐷)) → (A𝐹B) 𝐸)

Theoremcaovcld 5596* Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((φ (x 𝐶 y 𝐷)) → (x𝐹y) 𝐸)    &   (φA 𝐶)    &   (φB 𝐷)       (φ → (A𝐹B) 𝐸)

Theoremcaovcl 5597* Convert an operation closure law to class notation. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
((x 𝑆 y 𝑆) → (x𝐹y) 𝑆)       ((A 𝑆 B 𝑆) → (A𝐹B) 𝑆)

Theoremcaovcomg 5598* Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.)
((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))       ((φ (A 𝑆 B 𝑆)) → (A𝐹B) = (B𝐹A))

Theoremcaovcomd 5599* Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))    &   (φA 𝑆)    &   (φB 𝑆)       (φ → (A𝐹B) = (B𝐹A))

Theoremcaovcom 5600* Convert an operation commutative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
A V    &   B V    &   (x𝐹y) = (y𝐹x)       (A𝐹B) = (B𝐹A)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9427
 Copyright terms: Public domain < Previous  Next >