P. 57 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 5601-5700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ovg 5601*	The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   &   |- ((ta /\ (x e. R /\ y e. S)) -> E!zph)   &   |- F = {<.<.x, y>., z>. | ((x e. R /\ y e. S) /\ ph)}   =>   |- ((ta /\ (A e. R /\ B e. S /\ C e. D)) -> ((AFB) = C <-> th))
Theorem	ovres 5602	The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
|- ((A e. C /\ B e. D) -> (A(F |` (C X. D))B) = (AFB))
Theorem	oprssov 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 X. D) /\ G C_ F) /\ (A e. C /\ B e. D)) -> (AFB) = (AGB))
Theorem	fovrn 5604	A operations's value belongs to its codomain. (Contributed by set.mm contributors, 27-Aug-2006.)
|- ((F:(R X. S)-->C /\ A e. R /\ B e. S) -> (AFB) e. C)
Theorem	fnrnov 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 X. B) -> ran F = {z | E.x e. A E.y e. B z = (xFy)})
Theorem	foov 5606*	An onto mapping of an operation expressed in terms of operation values. (Contributed by set.mm contributors, 29-Oct-2006.)
|- (F:(A X. B)-onto->C <-> (F:(A X. B)-->C /\ A.z e. C E.x e. A E.y e. B z = (xFy)))
Theorem	fnovrn 5607	An operation's value belongs to its range. (Contributed by set.mm contributors, 10-Feb-2007.)
|- ((F Fn (A X. B) /\ C e. A /\ D e. B) -> (CFD) e. ran F)
Theorem	ovelrn 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 X. B) -> (C e. ran F <-> E.x e. A E.y e. B C = (xFy)))
Theorem	funimassov 5609*	Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
|- ((Fun F /\ (A X. B) C_ dom F) -> ((F"(A X. B)) C_ C <-> A.x e. A A.y e. B (xFy) e. C))
Theorem	ovelimab 5610*	Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013.)
|- ((F Fn A /\ (B X. C) C_ A) -> (D e. (F"(B X. C)) <-> E.x e. B E.y e. C D = (xFy)))
Theorem	ovconst2 5611	The value of a constant operation. (Contributed by set.mm contributors, 5-Nov-2006.)
|- C e. _V   =>   |- ((R e. A /\ S e. B) -> (R((A X. B) X. {C})S) = C)
Theorem	oprssdm 5612*	Domain of closure of an operation. (Contributed by set.mm contributors, 24-Aug-1995.)
|- -. (/) e. S   &   |- ((x e. S /\ y e. S) -> (xFy) e. S)   =>   |- (S X. S) C_ dom F
Theorem	ndmovg 5613	The value of an operation outside its domain. (Contributed by set.mm contributors, 28-Mar-2008.)
|- ((dom F = (R X. S) /\ -. (A e. R /\ B e. S)) -> (AFB) = (/))
Theorem	ndmovcl 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 X. S)   &   |- ((A e. S /\ x e. S) -> (AFx) e. S)   &   |- (/) e. S   =>   |- (AFB) e. S
Theorem	ndmov 5615	The value of an operation outside its domain. (Contributed by set.mm contributors, 24-Aug-1995.)
|- B e. _V   &   |- dom F = (S X. S)   =>   |- (-. (A e. S /\ B e. S) -> (AFB) = (/))
Theorem	ndmovrcl 5616	Reverse closure law, when an operation's domain doesn't contain the empty set. (Contributed by set.mm contributors, 3-Feb-1996.)
|- B e. _V   &   |- dom F = (S X. S)   &   |- -. (/) e. S   =>   |- ((AFB) e. S -> (A e. S /\ B e. S))
Theorem	ndmovcom 5617	Any operation is commutative outside its domain. (Contributed by set.mm contributors, 24-Aug-1995.)
|- B e. _V   &   |- dom F = (S X. S)   &   |- A e. _V   =>   |- (-. (A e. S /\ B e. S) -> (AFB) = (BFA))
Theorem	ndmovass 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 e. _V   &   |- dom F = (S X. S)   &   |- C e. _V   &   |- -. (/) e. S   =>   |- (-. (A e. S /\ B e. S /\ C e. S) -> ((AFB)FC) = (AF(BFC)))
Theorem	ndmovdistr 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 e. _V   &   |- dom F = (S X. S)   &   |- C e. _V   &   |- -. (/) e. S   &   |- dom G = (S X. S)   =>   |- (-. (A e. S /\ B e. S /\ C e. S) -> (AG(BFC)) = ((AGB)F(AGC)))
Theorem	ndmovord 5620	Elimination of redundant antecedents in an ordering law. (Contributed by set.mm contributors, 7-Mar-1996.)
|- B e. _V   &   |- dom F = (S X. S)   &   |- A e. _V   &   |- R C_ (S X. S)   &   |- -. (/) e. S   &   |- ((A e. S /\ B e. S /\ C e. S) -> (ARB <-> (CFA)R(CFB)))   =>   |- (C e. S -> (ARB <-> (CFA)R(CFB)))
Theorem	ndmovordi 5621	Elimination of redundant antecedent in an ordering law. (Contributed by set.mm contributors, 25-Jun-1998.)
|- A e. _V   &   |- dom F = (S X. S)   &   |- R C_ (S X. S)   &   |- -. (/) e. S   &   |- (C e. S -> (ARB <-> (CFA)R(CFB)))   =>   |- ((CFA)R(CFB) -> ARB)
Theorem	caovcld 5622*	Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.)
|- ((ph /\ (x e. C /\ y e. D)) -> (xFy) e. E)   =>   |- ((ph /\ (A e. C /\ B e. D)) -> (AFB) e. E)
Theorem	caovcl 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 e. S /\ y e. S) -> (xFy) e. S)   =>   |- ((A e. S /\ B e. S) -> (AFB) e. S)
Theorem	caovcomg 5624*	Convert an operation commutative law to class notation. (Contributed by set.mm contributors, 1-Jun-2013.) (Revised by Mario Carneiro, 2-Jun-2013.)
|- ((ph /\ (x e. S /\ y e. S)) -> (xFy) = (yFx))   =>   |- ((ph /\ (A e. S /\ B e. S)) -> (AFB) = (BFA))
Theorem	caovcom 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 e. _V   &   |- B e. _V   &   |- (xFy) = (yFx)   =>   |- (AFB) = (BFA)
Theorem	caovassg 5626*	Convert an operation associative law to class notation. (Contributed by set.mm contributors, 1-Jun-2013.) (Revised by Mario Carneiro, 2-Jun-2013.)
|- ((ph /\ (x e. S /\ y e. S /\ z e. S)) -> ((xFy)Fz) = (xF(yFz)))   =>   |- ((ph /\ (A e. S /\ B e. S /\ C e. S)) -> ((AFB)FC) = (AF(BFC)))
Theorem	caovass 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 e. _V   &   |- B e. _V   &   |- C e. _V   &   |- ((xFy)Fz) = (xF(yFz))   =>   |- ((AFB)FC) = (AF(BFC))
Theorem	caovcan 5628*	Convert an operation cancellation law to class notation. (Contributed by set.mm contributors, 20-Aug-1995.)
|- C e. _V   &   |- ((x e. S /\ y e. S) -> ((xFy) = (xFz) -> y = z))   =>   |- ((A e. S /\ B e. S) -> ((AFB) = (AFC) -> B = C))
Theorem	caovord 5629*	Convert an operation ordering law to class notation. (Contributed by set.mm contributors, 19-Feb-1996.)
|- A e. _V   &   |- B e. _V   &   |- (z e. S -> (xRy <-> (zFx)R(zFy)))   =>   |- (C e. S -> (ARB <-> (CFA)R(CFB)))
Theorem	caovord2 5630*	Operation ordering law with commuted arguments. (Contributed by set.mm contributors, 27-Feb-1996.)
|- A e. _V   &   |- B e. _V   &   |- (z e. S -> (xRy <-> (zFx)R(zFy)))   &   |- C e. _V   &   |- (xFy) = (yFx)   =>   |- (C e. S -> (ARB <-> (AFC)R(BFC)))
Theorem	caovord3 5631*	Ordering law. (Contributed by set.mm contributors, 29-Feb-1996.)
|- A e. _V   &   |- B e. _V   &   |- (z e. S -> (xRy <-> (zFx)R(zFy)))   &   |- C e. _V   &   |- (xFy) = (yFx)   &   |- D e. _V   =>   |- (((B e. S /\ C e. S) /\ (AFB) = (CFD)) -> (ARC <-> DRB))
Theorem	caovdig 5632*	Convert an operation distributive law to class notation. (Contributed by set.mm contributors, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
|- ((ph /\ (x e. S /\ y e. S /\ z e. S)) -> (xG(yFz)) = ((xGy)F(xGz)))   =>   |- ((ph /\ (A e. S /\ B e. S /\ C e. S)) -> (AG(BFC)) = ((AGB)F(AGC)))
Theorem	caovdirg 5633*	Convert an operation reverse distributive law to class notation. (Contributed by set.mm contributors, 19-Oct-2014.)
|- ((ph /\ (x e. S /\ y e. S /\ z e. S)) -> ((xFy)Gz) = ((xGz)F(yGz)))   =>   |- ((ph /\ (A e. S /\ B e. S /\ C e. S)) -> ((AFB)GC) = ((AGC)F(BGC)))
Theorem	caovdi 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 e. _V   &   |- B e. _V   &   |- C e. _V   &   |- (xG(yFz)) = ((xGy)F(xGz))   =>   |- (AG(BFC)) = ((AGB)F(AGC))
Theorem	caov32 5635*	Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- (xFy) = (yFx)   &   |- ((xFy)Fz) = (xF(yFz))   =>   |- ((AFB)FC) = ((AFC)FB)
Theorem	caov12 5636*	Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- (xFy) = (yFx)   &   |- ((xFy)Fz) = (xF(yFz))   =>   |- (AF(BFC)) = (BF(AFC))
Theorem	caov31 5637*	Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- (xFy) = (yFx)   &   |- ((xFy)Fz) = (xF(yFz))   =>   |- ((AFB)FC) = ((CFB)FA)
Theorem	caov13 5638*	Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- (xFy) = (yFx)   &   |- ((xFy)Fz) = (xF(yFz))   =>   |- (AF(BFC)) = (CF(BFA))
Theorem	caov4 5639*	Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- (xFy) = (yFx)   &   |- ((xFy)Fz) = (xF(yFz))   &   |- D e. _V   =>   |- ((AFB)F(CFD)) = ((AFC)F(BFD))
Theorem	caov411 5640*	Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- (xFy) = (yFx)   &   |- ((xFy)Fz) = (xF(yFz))   &   |- D e. _V   =>   |- ((AFB)F(CFD)) = ((CFB)F(AFD))
Theorem	caov42 5641*	Rearrange arguments in a commutative, associative operation. (Contributed by set.mm contributors, 26-Aug-1995.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- (xFy) = (yFx)   &   |- ((xFy)Fz) = (xF(yFz))   &   |- D e. _V   =>   |- ((AFB)F(CFD)) = ((AFC)F(DFB))
Theorem	caovdir 5642*	Reverse distributive law. (Contributed by set.mm contributors, 26-Aug-1995.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- (xGy) = (yGx)   &   |- (xG(yFz)) = ((xGy)F(xGz))   =>   |- ((AFB)GC) = ((AGC)F(BGC))
Theorem	caovdilem 5643*	Lemma used by real number construction. (Contributed by set.mm contributors, 26-Aug-1995.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- (xGy) = (yGx)   &   |- (xG(yFz)) = ((xGy)F(xGz))   &   |- D e. _V   &   |- H e. _V   &   |- ((xGy)Gz) = (xG(yGz))   =>   |- (((AGC)F(BGD))GH) = ((AG(CGH))F(BG(DGH)))
Theorem	caovlem2 5644*	Lemma used in real number construction. (Contributed by set.mm contributors, 26-Aug-1995.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- (xGy) = (yGx)   &   |- (xG(yFz)) = ((xGy)F(xGz))   &   |- D e. _V   &   |- H e. _V   &   |- ((xGy)Gz) = (xG(yGz))   &   |- R e. _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))))
Theorem	caovmo 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 e. _V   &   |- B e. S   &   |- dom F = (S X. S)   &   |- -. (/) e. S   &   |- (xFy) = (yFx)   &   |- ((xFy)Fz) = (xF(yFz))   &   |- (x e. S -> (xFB) = x)   =>   |- E*w(AFw) = B
Theorem	oprabid2 5646*	Identity law for operator abstractions. (Contributed by Scott Fenton, 19-Apr-2021.)
|- {<.<.x, y>., z>. | <.<.x, y>., z>. e. A} = A
Theorem	oprabbi2i 5647*	Biconditional for operators. (Contributed by Scott Fenton, 19-Apr-2021.)
|- (<.<.x, y>., z>. e. A <-> ph)   =>   |- A = {<.<.x, y>., z>. | ph}
Theorem	elovex12 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 e. (BFC) -> (B e. _V /\ C e. _V))
Theorem	elovex1 5649	Eliminate antecedent for operator values: domain can be taken to be a set. (Contributed by set.mm contributors, 25-Feb-2015.)
|- (A e. (BFC) -> B e. _V)
Theorem	elovex2 5650	Eliminate antecedent for operator values: range can be taken to be a set. (Contributed by set.mm contributors, 25-Feb-2015.)
|- (A e. (BFC) -> C e. _V)
2.3.9  "Maps to" notation
Syntax	cmpt 5651	Extend the definition of a class to include maps-to notation for defining a function via a rule.
class (x e. A |-> B)
Definition	df-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 e. A |-> B) = {<.x, y>. | (x e. A /\ y = B)}
Syntax	cmpt2 5653	Extend the definition of a class to include maps-to notation for defining an operation via a rule.
class (x e. A, y e. B |-> C)
Definition	df-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 X. B) to B(x, y)." An extension of df-mpt 5652 for two arguments. (Contributed by SF, 5-Jan-2015.)
|- (x e. A, y e. B |-> C) = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ z = C)}
Theorem	mpteq12f 5655	An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- ((A.x A = C /\ A.x e. A B = D) -> (x e. A |-> B) = (x e. C |-> D))
Theorem	mpteq12dv 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.)
|- (ph -> A = C)   &   |- (ph -> B = D)   =>   |- (ph -> (x e. A |-> B) = (x e. C |-> D))
Theorem	mpteq12 5657*	An equality theorem for the maps to notation. (Contributed by set.mm contributors, 16-Dec-2013.)
|- ((A = C /\ A.x e. A B = D) -> (x e. A |-> B) = (x e. C |-> D))
Theorem	mpteq1 5658*	An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- (A = B -> (x e. A |-> C) = (x e. B |-> C))
Theorem	mpteq2ia 5659	An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- (x e. A -> B = C)   =>   |- (x e. A |-> B) = (x e. A |-> C)
Theorem	mpteq2i 5660	An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- B = C   =>   |- (x e. A |-> B) = (x e. A |-> C)
Theorem	mpt2eq123 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 /\ A.x e. A (B = E /\ A.y e. B C = F)) -> (x e. A, y e. B |-> C) = (x e. D, y e. E |-> F))
Theorem	mpt2eq12 5662*	An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- ((A = C /\ B = D) -> (x e. A, y e. B |-> E) = (x e. C, y e. D |-> E))
Theorem	mpt2eq123dv 5663*	An equality deduction for the maps to notation. (Contributed by set.mm contributors, 12-Sep-2011.)
|- (ph -> A = D)   &   |- (ph -> B = E)   &   |- (ph -> C = F)   =>   |- (ph -> (x e. A, y e. B |-> C) = (x e. D, y e. E |-> F))
Theorem	mpt2eq123i 5664	An equality inference for the maps to notation. (Contributed by set.mm contributors, 15-Jul-2013.)
|- A = D   &   |- B = E   &   |- C = F   =>   |- (x e. A, y e. B |-> C) = (x e. D, y e. E |-> F)
Theorem	mpteq12i 5665	An equality inference for the maps to notation. (Contributed by Scott Fenton, 27-Oct-2010.)
|- A = C   &   |- B = D   =>   |- (x e. A |-> B) = (x e. C |-> D)
Theorem	mpteq2da 5666	Slightly more general equality inference for the maps to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
|- F/xph   &   |- ((ph /\ x e. A) -> B = C)   =>   |- (ph -> (x e. A |-> B) = (x e. A |-> C))
Theorem	mpteq2dva 5667*	Slightly more general equality inference for the maps to notation. (Contributed by Scott Fenton, 25-Apr-2012.)
|- ((ph /\ x e. A) -> B = C)   =>   |- (ph -> (x e. A |-> B) = (x e. A |-> C))
Theorem	mpteq2dv 5668*	An equality inference for the maps to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
|- (ph -> B = C)   =>   |- (ph -> (x e. A |-> B) = (x e. A |-> C))
Theorem	mpt2eq3dva 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.)
|- ((ph /\ x e. A /\ y e. B) -> C = D)   =>   |- (ph -> (x e. A, y e. B |-> C) = (x e. A, y e. B |-> D))
Theorem	mpt2eq3ia 5670	An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
|- ((x e. A /\ y e. B) -> C = D)   =>   |- (x e. A, y e. B |-> C) = (x e. A, y e. B |-> D)
Theorem	nfmpt 5671*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
|- F/_xA   &   |- F/_xB   =>   |- F/_x(y e. A |-> B)
Theorem	nfmpt1 5672	Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
|- F/_x(x e. A |-> B)
Theorem	nfmpt21 5673	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
|- F/_x(x e. A, y e. B |-> C)
Theorem	nfmpt22 5674	Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)
|- F/_y(x e. A, y e. B |-> C)
Theorem	nfmpt2 5675*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
|- F/_zA   &   |- F/_zB   &   |- F/_zC   =>   |- F/_z(x e. A, y e. B |-> C)
Theorem	cbvmpt 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.)
|- F/_yB   &   |- F/_xC   &   |- (x = y -> B = C)   =>   |- (x e. A |-> B) = (y e. A |-> C)
Theorem	cbvmptv 5677*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.)
|- (x = y -> B = C)   =>   |- (x e. A |-> B) = (y e. A |-> C)
Theorem	cbvmpt2x 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.)
|- F/_zB   &   |- F/_xD   &   |- F/_zC   &   |- F/_wC   &   |- F/_xE   &   |- F/_yE   &   |- (x = z -> B = D)   &   |- ((x = z /\ y = w) -> C = E)   =>   |- (x e. A, y e. B |-> C) = (z e. A, w e. D |-> E)
Theorem	cbvmpt2 5679*	Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.)
|- F/_zC   &   |- F/_wC   &   |- F/_xD   &   |- F/_yD   &   |- ((x = z /\ y = w) -> C = D)   =>   |- (x e. A, y e. B |-> C) = (z e. A, w e. B |-> D)
Theorem	cbvmpt2v 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 = z -> C = E)   &   |- (y = w -> E = D)   =>   |- (x e. A, y e. B |-> C) = (z e. A, w e. B |-> D)
Theorem	fconstmpt 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 X. {B}) = (x e. A |-> B)
Theorem	mptpreima 5682*	The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- F = (x e. A |-> B)   =>   |- (`'F"C) = {x e. A | B e. C}
Theorem	dmmpt 5683	The domain of the mapping operation in general. (Contributed by Mario Carneiro, 13-Sep-2013.)
|- F = (x e. A |-> B)   =>   |- dom F = {x e. A | B e. _V}
Theorem	dmmptg 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.)
|- (A.x e. A B e. V -> dom (x e. A |-> B) = A)
Theorem	dmmptss 5685*	The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.)
|- F = (x e. A |-> B)   =>   |- dom F C_ A
Theorem	rnmpt 5686*	The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011.)
|- F = (x e. A |-> B)   =>   |- ran F = {y | E.x e. A y = B}
Theorem	funmpt 5687	A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.)
|- Fun (x e. A |-> B)
Theorem	mptfng 5688*	The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011.)
|- F = (x e. A |-> B)   =>   |- (A.x e. A B e. _V <-> F Fn A)
Theorem	fnmpt 5689*	The maps-to notation defines a function with domain. (Contributed by set.mm contributors, 9-Apr-2013.)
|- F = (x e. A |-> B)   =>   |- (A.x e. A B e. V -> F Fn A)
Theorem	fnmpti 5690*	Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- B e. _V   &   |- F = (x e. A |-> B)   =>   |- F Fn A
Theorem	dmmpti 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 e. _V   &   |- F = (x e. A |-> B)   =>   |- dom F = A
Theorem	fmpt 5692*	Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- F = (x e. A |-> C)   =>   |- (A.x e. A C e. B <-> F:A-->B)
Theorem	fmpti 5693*	Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- F = (x e. A |-> C)   &   |- (x e. A -> C e. B)   =>   |- F:A-->B
Theorem	fmptd 5694*	Domain and co-domain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)
|- ((ph /\ x e. A) -> B e. C)   &   |- F = (x e. A |-> B)   =>   |- (ph -> F:A-->C)
Theorem	fmpt2d 5695*	Domain and co-domain of the mapping operation; deduction form. (Contributed by set.mm contributors, 9-Apr-2013.)
|- (ph -> (x e. A -> B e. V))   &   |- F = (x e. A |-> B)   &   |- (ph -> (y e. A -> (F` y) e. C))   =>   |- (ph -> F:A-->C)
Theorem	resmpt 5696*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 15-Jul-2013.)
|- (B C_ A -> ((x e. A |-> C) |` B) = (x e. B |-> C))
Theorem	resmpt2 5697*	Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)
|- ((C C_ A /\ D C_ B) -> ((x e. A, y e. B |-> E) |` (C X. D)) = (x e. C, y e. D |-> E))
Theorem	fvmptg 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 = A -> B = C)   &   |- F = (x e. D |-> B)   =>   |- ((A e. D /\ C e. R) -> (F` A) = C)
Theorem	fvmpti 5699*	Value of a function given in maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014.)
|- (x = A -> B = C)   &   |- F = (x e. D |-> B)   =>   |- (A e. D -> (F` A) = ( _I ` C))
Theorem	fvmpt 5700*	Value of a function given in maps-to notation. (Contributed by set.mm contributors, 17-Aug-2011.)
|- (x = A -> B = C)   &   |- F = (x e. D |-> B)   &   |- C e. _V   =>   |- (A e. D -> (F` A) = C)