HomeHome New Foundations Explorer
Theorem List (p. 57 of 64)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 5601-5700   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremovg 5601* The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
(x = A → (φψ))    &   (y = B → (ψχ))    &   (z = C → (χθ))    &   ((τ (x R y S)) → ∃!zφ)    &   F = {x, y, z ((x R y S) φ)}       ((τ (A R B S C D)) → ((AFB) = Cθ))
 
Theoremovres 5602 The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
((A C B D) → (A(F (C × D))B) = (AFB))
 
Theoremoprssov 5603 The value of a member of the domain of a subclass of an operation. (Contributed by set.mm contributors, 23-Aug-2007.)
(((Fun F G Fn (C × D) G F) (A C B D)) → (AFB) = (AGB))
 
Theoremfovrn 5604 A operations's value belongs to its codomain. (Contributed by set.mm contributors, 27-Aug-2006.)
((F:(R × S)–→C A R B S) → (AFB) C)
 
Theoremfnrnov 5605* The range of an operation expressed as a collection of the operation's values. (Contributed by set.mm contributors, 29-Oct-2006.)
(F Fn (A × B) → ran F = {z x A y B z = (xFy)})
 
Theoremfoov 5606* An onto mapping of an operation expressed in terms of operation values. (Contributed by set.mm contributors, 29-Oct-2006.)
(F:(A × B)–ontoC ↔ (F:(A × B)–→C z C x A y B z = (xFy)))
 
Theoremfnovrn 5607 An operation's value belongs to its range. (Contributed by set.mm contributors, 10-Feb-2007.)
((F Fn (A × B) C A D B) → (CFD) ran F)
 
Theoremovelrn 5608* A member of an operation's range is a value of the operation. (Contributed by set.mm contributors, 7-Feb-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
(F Fn (A × B) → (C ran Fx A y B C = (xFy)))
 
Theoremfunimassov 5609* Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
((Fun F (A × B) dom F) → ((F “ (A × B)) Cx A y B (xFy) C))
 
Theoremovelimab 5610* Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013.)
((F Fn A (B × C) A) → (D (F “ (B × C)) ↔ x B y C D = (xFy)))
 
Theoremovconst2 5611 The value of a constant operation. (Contributed by set.mm contributors, 5-Nov-2006.)
C V       ((R A S B) → (R((A × B) × {C})S) = C)
 
Theoremoprssdm 5612* Domain of closure of an operation. (Contributed by set.mm contributors, 24-Aug-1995.)
¬ S    &   ((x S y S) → (xFy) S)       (S × S) dom F
 
Theoremndmovg 5613 The value of an operation outside its domain. (Contributed by set.mm contributors, 28-Mar-2008.)
((dom F = (R × S) ¬ (A R B S)) → (AFB) = )
 
Theoremndmovcl 5614* The closure of an operation outside its domain, when the domain includes the empty set. This technical lemma can make the operation more convenient to work in some cases. It is is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by set.mm contributors, 24-Sep-2004.)
dom F = (S × S)    &   ((A S x S) → (AFx) S)    &    S       (AFB) S
 
Theoremndmov 5615 The value of an operation outside its domain. (Contributed by set.mm contributors, 24-Aug-1995.)
B V    &   dom F = (S × S)       (¬ (A S B S) → (AFB) = )
 
Theoremndmovrcl 5616 Reverse closure law, when an operation's domain doesn't contain the empty set. (Contributed by set.mm contributors, 3-Feb-1996.)
B V    &   dom F = (S × S)    &    ¬ S       ((AFB) S → (A S B S))
 
Theoremndmovcom 5617 Any operation is commutative outside its domain. (Contributed by set.mm contributors, 24-Aug-1995.)
B V    &   dom F = (S × S)    &   A V       (¬ (A S B S) → (AFB) = (BFA))
 
Theoremndmovass 5618 Any operation is associative outside its domain, if the domain doesn't contain the empty set. (Contributed by set.mm contributors, 24-Aug-1995.)
B V    &   dom F = (S × S)    &   C V    &    ¬ S       (¬ (A S B S C S) → ((AFB)FC) = (AF(BFC)))
 
Theoremndmovdistr 5619 Any operation is distributive outside its domain, if the domain doesn't contain the empty set. (Contributed by set.mm contributors, 24-Aug-1995.)
B V    &   dom F = (S × S)    &   C V    &    ¬ S    &   dom G = (S × S)       (¬ (A S B S C S) → (AG(BFC)) = ((AGB)F(AGC)))
 
Theoremndmovord 5620 Elimination of redundant antecedents in an ordering law. (Contributed by set.mm contributors, 7-Mar-1996.)
B V    &   dom F = (S × S)    &   A V    &   R (S × S)    &    ¬ S    &   ((A S B S C S) → (ARB ↔ (CFA)R(CFB)))       (C S → (ARB ↔ (CFA)R(CFB)))
 
Theoremndmovordi 5621 Elimination of redundant antecedent in an ordering law. (Contributed by set.mm contributors, 25-Jun-1998.)
A V    &   dom F = (S × S)    &   R (S × S)    &    ¬ S    &   (C S → (ARB ↔ (CFA)R(CFB)))       ((CFA)R(CFB) → ARB)
 
Theoremcaovcld 5622* Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.)
((φ (x C y D)) → (xFy) E)       ((φ (A C B D)) → (AFB) E)
 
Theoremcaovcl 5623* Convert an operation closure law to class notation. (Contributed by set.mm contributors, 4-Aug-1995.) (Revised by set.mm contributors, 26-May-2014.)
((x S y S) → (xFy) S)       ((A S B S) → (AFB) S)
 
Theoremcaovcomg 5624* Convert an operation commutative law to class notation. (Contributed by set.mm contributors, 1-Jun-2013.) (Revised by Mario Carneiro, 2-Jun-2013.)
((φ (x S y S)) → (xFy) = (yFx))       ((φ (A S B S)) → (AFB) = (BFA))
 
Theoremcaovcom 5625* Convert an operation commutative law to class notation. (Contributed by set.mm contributors, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
A V    &   B V    &   (xFy) = (yFx)       (AFB) = (BFA)
 
Theoremcaovassg 5626* Convert an operation associative law to class notation. (Contributed by set.mm contributors, 1-Jun-2013.) (Revised by Mario Carneiro, 2-Jun-2013.)
((φ (x S y S z S)) → ((xFy)Fz) = (xF(yFz)))       ((φ (A S B S C S)) → ((AFB)FC) = (AF(BFC)))
 
Theoremcaovass 5627* Convert an operation associative law to class notation. (Contributed by set.mm contributors, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
A V    &   B V    &   C V    &   ((xFy)Fz) = (xF(yFz))       ((AFB)FC) = (AF(BFC))
 
Theoremcaovcan 5628* Convert an operation cancellation law to class notation. (Contributed by set.mm contributors, 20-Aug-1995.)
C V    &   ((x S y S) → ((xFy) = (xFz) → y = z))       ((A S B S) → ((AFB) = (AFC) → B = C))
 
Theoremcaovord 5629* Convert an operation ordering law to class notation. (Contributed by set.mm contributors, 19-Feb-1996.)
A V    &   B V    &   (z S → (xRy ↔ (zFx)R(zFy)))       (C S → (ARB ↔ (CFA)R(CFB)))
 
Theoremcaovord2 5630* Operation ordering law with commuted arguments. (Contributed by set.mm contributors, 27-Feb-1996.)
A V    &   B V    &   (z S → (xRy ↔ (zFx)R(zFy)))    &   C V    &   (xFy) = (yFx)       (C S → (ARB ↔ (AFC)R(BFC)))
 
Theoremcaovord3 5631* Ordering law. (Contributed by set.mm contributors, 29-Feb-1996.)
A V    &   B V    &   (z S → (xRy ↔ (zFx)R(zFy)))    &   C V    &   (xFy) = (yFx)    &   D V       (((B S C S) (AFB) = (CFD)) → (ARCDRB))
 
Theoremcaovdig 5632* Convert an operation distributive law to class notation. (Contributed by set.mm contributors, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
((φ (x S y S z S)) → (xG(yFz)) = ((xGy)F(xGz)))       ((φ (A S B S C S)) → (AG(BFC)) = ((AGB)F(AGC)))
 
Theoremcaovdirg 5633* Convert an operation reverse distributive law to class notation. (Contributed by set.mm contributors, 19-Oct-2014.)
((φ (x S y S z S)) → ((xFy)Gz) = ((xGz)F(yGz)))       ((φ (A S B S C S)) → ((AFB)GC) = ((AGC)F(BGC)))
 
Theoremcaovdi 5634* Convert an operation distributive law to class notation. (Contributed by set.mm contributors, 25-Aug-1995.) (Revised by Mario Carneiro, 28-Jun-2013.)
A V    &   B V    &   C V    &   (xG(yFz)) = ((xGy)F(xGz))       (AG(BFC)) = ((AGB)F(AGC))
 
Theoremcaov32 5635* Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
A V    &   B V    &   C V    &   (xFy) = (yFx)    &   ((xFy)Fz) = (xF(yFz))       ((AFB)FC) = ((AFC)FB)
 
Theoremcaov12 5636* Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
A V    &   B V    &   C V    &   (xFy) = (yFx)    &   ((xFy)Fz) = (xF(yFz))       (AF(BFC)) = (BF(AFC))
 
Theoremcaov31 5637* Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
A V    &   B V    &   C V    &   (xFy) = (yFx)    &   ((xFy)Fz) = (xF(yFz))       ((AFB)FC) = ((CFB)FA)
 
Theoremcaov13 5638* Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
A V    &   B V    &   C V    &   (xFy) = (yFx)    &   ((xFy)Fz) = (xF(yFz))       (AF(BFC)) = (CF(BFA))
 
Theoremcaov4 5639* Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
A V    &   B V    &   C V    &   (xFy) = (yFx)    &   ((xFy)Fz) = (xF(yFz))    &   D V       ((AFB)F(CFD)) = ((AFC)F(BFD))
 
Theoremcaov411 5640* Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
A V    &   B V    &   C V    &   (xFy) = (yFx)    &   ((xFy)Fz) = (xF(yFz))    &   D V       ((AFB)F(CFD)) = ((CFB)F(AFD))
 
Theoremcaov42 5641* Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
A V    &   B V    &   C V    &   (xFy) = (yFx)    &   ((xFy)Fz) = (xF(yFz))    &   D V       ((AFB)F(CFD)) = ((AFC)F(DFB))
 
Theoremcaovdir 5642* Reverse distributive law. (Contributed by set.mm contributors, 26-Aug-1995.)
A V    &   B V    &   C V    &   (xGy) = (yGx)    &   (xG(yFz)) = ((xGy)F(xGz))       ((AFB)GC) = ((AGC)F(BGC))
 
Theoremcaovdilem 5643* Lemma used by real number construction. (Contributed by set.mm contributors, 26-Aug-1995.)
A V    &   B V    &   C V    &   (xGy) = (yGx)    &   (xG(yFz)) = ((xGy)F(xGz))    &   D V    &   H V    &   ((xGy)Gz) = (xG(yGz))       (((AGC)F(BGD))GH) = ((AG(CGH))F(BG(DGH)))
 
Theoremcaovlem2 5644* Lemma used in real number construction. (Contributed by set.mm contributors, 26-Aug-1995.)
A V    &   B V    &   C V    &   (xGy) = (yGx)    &   (xG(yFz)) = ((xGy)F(xGz))    &   D V    &   H V    &   ((xGy)Gz) = (xG(yGz))    &   R V    &   (xFy) = (yFx)    &   ((xFy)Fz) = (xF(yFz))       ((((AGC)F(BGD))GH)F(((AGD)F(BGC))GR)) = ((AG((CGH)F(DGR)))F(BG((CGR)F(DGH))))
 
Theoremcaovmo 5645* Uniqueness of inverse element in commutative, associative operation with identity. Remark in proof of Proposition 9-2.4 of [Gleason] p. 119. (Contributed by set.mm contributors, 4-Mar-1996.)
A V    &   B S    &   dom F = (S × S)    &    ¬ S    &   (xFy) = (yFx)    &   ((xFy)Fz) = (xF(yFz))    &   (x S → (xFB) = x)       ∃*w(AFw) = B
 
Theoremoprabid2 5646* Identity law for operator abstractions. (Contributed by Scott Fenton, 19-Apr-2021.)
{x, y, z x, y, z A} = A
 
Theoremoprabbi2i 5647* Biconditional for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
(x, y, z Aφ)       A = {x, y, z φ}
 
Theoremelovex12 5648 Eliminate antecedent for operator values: domain and range can be taken to be a set. (Contributed by set.mm contributors, 25-Feb-2015.)
(A (BFC) → (B V C V))
 
Theoremelovex1 5649 Eliminate antecedent for operator values: domain can be taken to be a set. (Contributed by set.mm contributors, 25-Feb-2015.)
(A (BFC) → B V)
 
Theoremelovex2 5650 Eliminate antecedent for operator values: range can be taken to be a set. (Contributed by set.mm contributors, 25-Feb-2015.)
(A (BFC) → C V)
 
2.3.9  "Maps to" notation
 
Syntaxcmpt 5651 Extend the definition of a class to include maps-to notation for defining a function via a rule.
class (x A B)
 
Definitiondf-mpt 5652* Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from x (in A) to B(x)." The class expression B is the value of the function at x and normally contains the variable x. Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by SF, 5-Jan-2015.)
(x A B) = {x, y (x A y = B)}
 
Syntaxcmpt2 5653 Extend the definition of a class to include maps-to notation for defining an operation via a rule.
class (x A, y B C)
 
Definitiondf-mpt2 5654* Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x, y (in A × B) to B(x, y)." An extension of df-mpt 5652 for two arguments. (Contributed by SF, 5-Jan-2015.)
(x A, y B C) = {x, y, z ((x A y B) z = C)}
 
Theoremmpteq12f 5655 An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
((x A = C x A B = D) → (x A B) = (x C D))
 
Theoremmpteq12dv 5656* An equality inference for the maps to notation. (Contributed by set.mm contributors, 24-Aug-2011.) (Revised by set.mm contributors, 16-Dec-2013.)
(φA = C)    &   (φB = D)       (φ → (x A B) = (x C D))
 
Theoremmpteq12 5657* An equality theorem for the maps to notation. (Contributed by set.mm contributors, 16-Dec-2013.)
((A = C x A B = D) → (x A B) = (x C D))
 
Theoremmpteq1 5658* An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
(A = B → (x A C) = (x B C))
 
Theoremmpteq2ia 5659 An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
(x AB = C)       (x A B) = (x A C)
 
Theoremmpteq2i 5660 An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
B = C       (x A B) = (x A C)
 
Theoremmpt2eq123 5661* An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)
((A = D x A (B = E y B C = F)) → (x A, y B C) = (x D, y E F))
 
Theoremmpt2eq12 5662* An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
((A = C B = D) → (x A, y B E) = (x C, y D E))
 
Theoremmpt2eq123dv 5663* An equality deduction for the maps to notation. (Contributed by set.mm contributors, 12-Sep-2011.)
(φA = D)    &   (φB = E)    &   (φC = F)       (φ → (x A, y B C) = (x D, y E F))
 
Theoremmpt2eq123i 5664 An equality inference for the maps to notation. (Contributed by set.mm contributors, 15-Jul-2013.)
A = D    &   B = E    &   C = F       (x A, y B C) = (x D, y E F)
 
Theoremmpteq12i 5665 An equality inference for the maps to notation. (Contributed by Scott Fenton, 27-Oct-2010.)
A = C    &   B = D       (x A B) = (x C D)
 
Theoremmpteq2da 5666 Slightly more general equality inference for the maps to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
xφ    &   ((φ x A) → B = C)       (φ → (x A B) = (x A C))
 
Theoremmpteq2dva 5667* Slightly more general equality inference for the maps to notation. (Contributed by Scott Fenton, 25-Apr-2012.)
((φ x A) → B = C)       (φ → (x A B) = (x A C))
 
Theoremmpteq2dv 5668* An equality inference for the maps to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
(φB = C)       (φ → (x A B) = (x A C))
 
Theoremmpt2eq3dva 5669* Slightly more general equality inference for the maps to notation. (Contributed by set.mm contributors, 17-Oct-2013.) (Revised by set.mm contributors, 16-Dec-2013.)
((φ x A y B) → C = D)       (φ → (x A, y B C) = (x A, y B D))
 
Theoremmpt2eq3ia 5670 An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
((x A y B) → C = D)       (x A, y B C) = (x A, y B D)
 
Theoremnfmpt 5671* Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
xA    &   xB       x(y A B)
 
Theoremnfmpt1 5672 Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
x(x A B)
 
Theoremnfmpt21 5673 Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
x(x A, y B C)
 
Theoremnfmpt22 5674 Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
y(x A, y B C)
 
Theoremnfmpt2 5675* Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
zA    &   zB    &   zC       z(x A, y B C)
 
Theoremcbvmpt 5676* Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.)
yB    &   xC    &   (x = yB = C)       (x A B) = (y A C)
 
Theoremcbvmptv 5677* Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
(x = yB = C)       (x A B) = (y A C)
 
Theoremcbvmpt2x 5678* Rule to change the bound variable in a maps-to function, using implicit substitution. This version of cbvmpt2 5679 allows B to be a function of x. (Contributed by NM, 29-Dec-2014.)
zB    &   xD    &   zC    &   wC    &   xE    &   yE    &   (x = zB = D)    &   ((x = z y = w) → C = E)       (x A, y B C) = (z A, w D E)
 
Theoremcbvmpt2 5679* Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.)
zC    &   wC    &   xD    &   yD    &   ((x = z y = w) → C = D)       (x A, y B C) = (z A, w B D)
 
Theoremcbvmpt2v 5680* Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 5676, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.)
(x = zC = E)    &   (y = wE = D)       (x A, y B C) = (z A, w B D)
 
Theoremfconstmpt 5681* Representation of a constant function using the mapping operation. (Note that x cannot appear free in B.) (Contributed by set.mm contributors, 16-Nov-2013.)
(A × {B}) = (x A B)
 
Theoremmptpreima 5682* The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)
F = (x A B)       (FC) = {x A B C}
 
Theoremdmmpt 5683 The domain of the mapping operation in general. (Contributed by Mario Carneiro, 13-Sep-2013.)
F = (x A B)       dom F = {x A B V}
 
Theoremdmmptg 5684* The domain of the mapping operation is the stated domain, if the function value is always a set. (Contributed by Mario Carneiro, 9-Feb-2013.)
(x A B V → dom (x A B) = A)
 
Theoremdmmptss 5685* The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.)
F = (x A B)       dom F A
 
Theoremrnmpt 5686* The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011.)
F = (x A B)       ran F = {y x A y = B}
 
Theoremfunmpt 5687 A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.)
Fun (x A B)
 
Theoremmptfng 5688* The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011.)
F = (x A B)       (x A B V ↔ F Fn A)
 
Theoremfnmpt 5689* The maps-to notation defines a function with domain. (Contributed by set.mm contributors, 9-Apr-2013.)
F = (x A B)       (x A B VF Fn A)
 
Theoremfnmpti 5690* Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
B V    &   F = (x A B)       F Fn A
 
Theoremdmmpti 5691* Domain of an ordered-pair class abstraction that specifies a function. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 31-Aug-2015.)
B V    &   F = (x A B)       dom F = A
 
Theoremfmpt 5692* Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
F = (x A C)       (x A C BF:A–→B)
 
Theoremfmpti 5693* Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
F = (x A C)    &   (x AC B)       F:A–→B
 
Theoremfmptd 5694* Domain and co-domain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)
((φ x A) → B C)    &   F = (x A B)       (φF:A–→C)
 
Theoremfmpt2d 5695* Domain and co-domain of the mapping operation; deduction form. (Contributed by set.mm contributors, 9-Apr-2013.)
(φ → (x AB V))    &   F = (x A B)    &   (φ → (y A → (Fy) C))       (φF:A–→C)
 
Theoremresmpt 5696* Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.)
(B A → ((x A C) B) = (x B C))
 
Theoremresmpt2 5697* Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)
((C A D B) → ((x A, y B E) (C × D)) = (x C, y D E))
 
Theoremfvmptg 5698* Value of a function given in maps-to notation. Analogous to fvopab4g 5388. (Contributed by set.mm contributors, 2-Oct-2007.) (Revised by set.mm contributors, 4-Aug-2008.)
(x = AB = C)    &   F = (x D B)       ((A D C R) → (FA) = C)
 
Theoremfvmpti 5699* Value of a function given in maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014.)
(x = AB = C)    &   F = (x D B)       (A D → (FA) = ( I ‘C))
 
Theoremfvmpt 5700* Value of a function given in maps-to notation. (Contributed by set.mm contributors, 17-Aug-2011.)
(x = AB = C)    &   F = (x D B)    &   C V       (A D → (FA) = C)
    < Previous  Next >

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-6336
  Copyright terms: Public domain < Previous  Next >