P. 41 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4001-4100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	disjxsn 4001*	A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- Disj x e. { A } B
Theorem	disjx0 4002	An empty collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- Disj x e. (/) B
2.1.22  Binary relations
Syntax	wbr 4003	Extend wff notation to include the general binary relation predicate. Note that the syntax is simply three class symbols in a row. Since binary relations are the only possible wff expressions consisting of three class expressions in a row, the syntax is unambiguous.
wff A R B
Definition	df-br 4004	Define a general binary relation. Note that the syntax is simply three class symbols in a row. Definition 6.18 of [TakeutiZaring] p. 29 generalized to arbitrary classes. This definition of relations is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when R is a proper class (see for example iprc 4895). (Contributed by NM, 31-Dec-1993.)
|- ( A R B <-> <. A , B >. e. R )
Theorem	breq 4005	Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)
|- ( R = S -> ( A R B <-> A S B ) )
Theorem	breq1 4006	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
|- ( A = B -> ( A R C <-> B R C ) )
Theorem	breq2 4007	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
|- ( A = B -> ( C R A <-> C R B ) )
Theorem	breq12 4008	Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )
Theorem	breqi 4009	Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)
|- R = S   =>    |- ( A R B <-> A S B )
Theorem	breq1i 4010	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- A = B   =>    |- ( A R C <-> B R C )
Theorem	breq2i 4011	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- A = B   =>    |- ( C R A <-> C R B )
Theorem	breq12i 4012	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|- A = B   &    |- C = D   =>    |- ( A R C <-> B R D )
Theorem	breq1d 4013	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A R C <-> B R C ) )
Theorem	breqd 4014	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C A D <-> C B D ) )
Theorem	breq2d 4015	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C R A <-> C R B ) )
Theorem	breq12d 4016	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A R C <-> B R D ) )
Theorem	breq123d 4017	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
|- ( ph -> A = B )   &    |- ( ph -> R = S )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A R C <-> B S D ) )
Theorem	breqdi 4018	Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 5-Oct-2020.)
|- ( ph -> A = B )   &    |- ( ph -> C A D )   =>    |- ( ph -> C B D )
Theorem	breqan12d 4019	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ph -> A = B )   &    |- ( ps -> C = D )   =>    |- ( ( ph /\ ps ) -> ( A R C <-> B R D ) )
Theorem	breqan12rd 4020	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ph -> A = B )   &    |- ( ps -> C = D )   =>    |- ( ( ps /\ ph ) -> ( A R C <-> B R D ) )
Theorem	eqnbrtrd 4021	Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> A = B )   &    |- ( ph -> -. B R C )   =>    |- ( ph -> -. A R C )
Theorem	nbrne1 4022	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
|- ( ( A R B /\ -. A R C ) -> B =/= C )
Theorem	nbrne2 4023	Two classes are different if they don't have the same relationship to a third class. (Contributed by NM, 3-Jun-2012.)
|- ( ( A R C /\ -. B R C ) -> A =/= B )
Theorem	eqbrtri 4024	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- B R C   =>    |- A R C
Theorem	eqbrtrd 4025	Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)
|- ( ph -> A = B )   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	eqbrtrri 4026	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- A R C   =>    |- B R C
Theorem	eqbrtrrd 4027	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
|- ( ph -> A = B )   &    |- ( ph -> A R C )   =>    |- ( ph -> B R C )
Theorem	breqtri 4028	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- A R B   &    |- B = C   =>    |- A R C
Theorem	breqtrd 4029	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
|- ( ph -> A R B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A R C )
Theorem	breqtrri 4030	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- A R B   &    |- C = B   =>    |- A R C
Theorem	breqtrrd 4031	Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)
|- ( ph -> A R B )   &    |- ( ph -> C = B )   =>    |- ( ph -> A R C )
Theorem	3brtr3i 4032	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
|- A R B   &    |- A = C   &    |- B = D   =>    |- C R D
Theorem	3brtr4i 4033	Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)
|- A R B   &    |- C = A   &    |- D = B   =>    |- C R D
Theorem	3brtr3d 4034	Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)
|- ( ph -> A R B )   &    |- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> C R D )
Theorem	3brtr4d 4035	Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
|- ( ph -> A R B )   &    |- ( ph -> C = A )   &    |- ( ph -> D = B )   =>    |- ( ph -> C R D )
Theorem	3brtr3g 4036	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
|- ( ph -> A R B )   &    |- A = C   &    |- B = D   =>    |- ( ph -> C R D )
Theorem	3brtr4g 4037	Substitution of equality into both sides of a binary relation. (Contributed by NM, 16-Jan-1997.)
|- ( ph -> A R B )   &    |- C = A   &    |- D = B   =>    |- ( ph -> C R D )
Theorem	eqbrtrid 4038	B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
|- A = B   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	eqbrtrrid 4039	B chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)
|- B = A   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	breqtrid 4040	B chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
|- A R B   &    |- ( ph -> B = C )   =>    |- ( ph -> A R C )
Theorem	breqtrrid 4041	B chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
|- A R B   &    |- ( ph -> C = B )   =>    |- ( ph -> A R C )
Theorem	eqbrtrdi 4042	A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)
|- ( ph -> A = B )   &    |- B R C   =>    |- ( ph -> A R C )
Theorem	eqbrtrrdi 4043	A chained equality inference for a binary relation. (Contributed by NM, 4-Jan-2006.)
|- ( ph -> B = A )   &    |- B R C   =>    |- ( ph -> A R C )
Theorem	breqtrdi 4044	A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
|- ( ph -> A R B )   &    |- B = C   =>    |- ( ph -> A R C )
Theorem	breqtrrdi 4045	A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
|- ( ph -> A R B )   &    |- C = B   =>    |- ( ph -> A R C )
Theorem	ssbrd 4046	Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( C A D -> C B D ) )
Theorem	ssbri 4047	Inference from a subclass relationship of binary relations. (Contributed by NM, 28-Mar-2007.) (Revised by Mario Carneiro, 8-Feb-2015.)
|- A C_ B   =>    |- ( C A D -> C B D )
Theorem	nfbrd 4048	Deduction version of bound-variable hypothesis builder nfbr 4049. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x R )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A R B )
Theorem	nfbr 4049	Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x A   &    |- F/_ x R   &    |- F/_ x B   =>    |- F/ x A R B
Theorem	brab1 4050*	Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011.)
|- ( x R A <-> x e. { z | z R A } )
Theorem	br0 4051	The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.)
|- -. A (/) B
Theorem	brne0 4052	If two sets are in a binary relation, the relation cannot be empty. In fact, the relation is also inhabited, as seen at brm 4053. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
|- ( A R B -> R =/= (/) )
Theorem	brm 4053*	If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.)
|- ( A R B -> E. x x e. R )
Theorem	brun 4054	The union of two binary relations. (Contributed by NM, 21-Dec-2008.)
|- ( A ( R u. S ) B <-> ( A R B \/ A S B ) )
Theorem	brin 4055	The intersection of two relations. (Contributed by FL, 7-Oct-2008.)
|- ( A ( R i^i S ) B <-> ( A R B /\ A S B ) )
Theorem	brdif 4056	The difference of two binary relations. (Contributed by Scott Fenton, 11-Apr-2011.)
|- ( A ( R \ S ) B <-> ( A R B /\ -. A S B ) )
Theorem	sbcbrg 4057	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( A e. D -> ( [. A / x ]. B R C <-> [_ A / x ]_ B [_ A / x ]_ R [_ A / x ]_ C ) )
Theorem	sbcbr12g 4058*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- ( A e. D -> ( [. A / x ]. B R C <-> [_ A / x ]_ B R [_ A / x ]_ C ) )
Theorem	sbcbr1g 4059*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- ( A e. D -> ( [. A / x ]. B R C <-> [_ A / x ]_ B R C ) )
Theorem	sbcbr2g 4060*	Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005.)
|- ( A e. D -> ( [. A / x ]. B R C <-> B R [_ A / x ]_ C ) )
Theorem	brralrspcev 4061*	Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.)
|- ( ( B e. X /\ A. y e. Y A R B ) -> E. x e. X A. y e. Y A R x )
Theorem	brimralrspcev 4062*	Restricted existential specialization with a restricted universal quantifier over an implication with a relation in the antecedent, closed form. (Contributed by AV, 20-Aug-2022.)
|- ( ( B e. X /\ A. y e. Y ( ( ph /\ A R B ) -> ps ) ) -> E. x e. X A. y e. Y ( ( ph /\ A R x ) -> ps ) )
2.1.23  Ordered-pair class abstractions (class builders)
Syntax	copab 4063	Extend class notation to include ordered-pair class abstraction (class builder).
class { <. x , y >. | ph }
Syntax	cmpt 4064	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-opab 4065*	Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually x and y are distinct, although the definition doesn't strictly require it. The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by NM, 4-Jul-1994.)
|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
Definition	df-mpt 4066*	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 NM, 17-Feb-2008.)
|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
Theorem	opabss 4067*	The collection of ordered pairs in a class is a subclass of it. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- { <. x , y >. | x R y } C_ R
Theorem	opabbid 4068	Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 21-Feb-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { <. x , y >. | ps } = { <. x , y >. | ch } )
Theorem	opabbidv 4069*	Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { <. x , y >. | ps } = { <. x , y >. | ch } )
Theorem	opabbii 4070	Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
|- ( ph <-> ps )   =>    |- { <. x , y >. | ph } = { <. x , y >. | ps }
Theorem	nfopab 4071*	Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011.)
|- F/ z ph   =>    |- F/_ z { <. x , y >. | ph }
Theorem	nfopab1 4072	The first abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x { <. x , y >. | ph }
Theorem	nfopab2 4073	The second abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ y { <. x , y >. | ph }
Theorem	cbvopab 4074*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003.)
|- F/ z ph   &    |- F/ w ph   &    |- F/ x ps   &    |- F/ y ps   &    |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , w >. | ps }
Theorem	cbvopabv 4075*	Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.)
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , w >. | ps }
Theorem	cbvopab1 4076*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/ z ph   &    |- F/ x ps   &    |- ( x = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , y >. | ps }
Theorem	cbvopab2 4077*	Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013.)
|- F/ z ph   &    |- F/ y ps   &    |- ( y = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. x , z >. | ps }
Theorem	cbvopab1s 4078*	Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003.)
|- { <. x , y >. | ph } = { <. z , y >. | [ z / x ] ph }
Theorem	cbvopab1v 4079*	Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.)
|- ( x = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. z , y >. | ps }
Theorem	cbvopab2v 4080*	Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999.)
|- ( y = z -> ( ph <-> ps ) )   =>    |- { <. x , y >. | ph } = { <. x , z >. | ps }
Theorem	csbopabg 4081*	Move substitution into a class abstraction. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
|- ( A e. V -> [_ A / x ]_ { <. y , z >. | ph } = { <. y , z >. | [. A / x ]. ph } )
Theorem	unopab 4082	Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
|- ( { <. x , y >. | ph } u. { <. x , y >. | ps } ) = { <. x , y >. | ( ph \/ ps ) }
Theorem	mpteq12f 4083	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	mpteq12dva 4084*	An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)
|- ( ph -> A = C )   &    |- ( ( ph /\ x e. A ) -> B = D )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq12dv 4085*	An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
|- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq12 4086*	An equality theorem for the maps-to notation. (Contributed by NM, 16-Dec-2013.)
|- ( ( A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )
Theorem	mpteq1 4087*	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	mpteq1d 4088*	An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
|- ( ph -> A = B )   =>    |- ( ph -> ( x e. A |-> C ) = ( x e. B |-> C ) )
Theorem	mpteq2ia 4089	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 4090	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	mpteq12i 4091	An equality inference for the maps-to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.)
|- A = C   &    |- B = D   =>    |- ( x e. A |-> B ) = ( x e. C |-> D )
Theorem	mpteq2da 4092	Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )
Theorem	mpteq2dva 4093*	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 4094*	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	nfmpt 4095*	Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( y e. A |-> B )
Theorem	nfmpt1 4096	Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)
|- F/_ x ( x e. A |-> B )
Theorem	cbvmptf 4097*	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 Thierry Arnoux, 9-Mar-2017.)
|- F/_ x A   &    |- F/_ y A   &    |- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- ( x e. A |-> B ) = ( y e. A |-> C )
Theorem	cbvmpt 4098*	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/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- ( x e. A |-> B ) = ( y e. A |-> C )
Theorem	cbvmptv 4099*	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	mptv 4100*	Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.)
|- ( x e. _V |-> B ) = { <. x , y >. | y = B }