P. 42 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4101-4200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cbvdisjv 4101*	Change bound variables in a disjoint collection. (Contributed by Mario Carneiro, 11-Dec-2016.)
|- ( x = y -> B = C )   =>    |- (Disj x e. A B <-> Disj y e. A C )
Theorem	nfdisjv 4102*	Bound-variable hypothesis builder for disjoint collection. (Contributed by Jim Kingdon, 19-Aug-2018.)
|- F/_ y A   &    |- F/_ y B   =>    |- F/ yDisj x e. A B
Theorem	nfdisj1 4103	Bound-variable hypothesis builder for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- F/ xDisj x e. A B
Theorem	disjnim 4104*	If a collection B ( i ) for i e. A is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Jim Kingdon, 6-Oct-2022.)
|- ( i = j -> B = C )   =>    |- (Disj i e. A B -> A. i e. A A. j e. A ( i =/= j -> ( B i^i C ) = (/) ) )
Theorem	disjnims 4105*	If a collection B ( i ) for i e. A is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by Jim Kingdon, 7-Oct-2022.)
|- (Disj x e. A B -> A. i e. A A. j e. A ( i =/= j -> ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
Theorem	disji2 4106*	Property of a disjoint collection: if B ( X ) = C and B ( Y ) = D, and X =/= Y, then C and D are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- ( x = X -> B = C )   &    |- ( x = Y -> B = D )   =>    |- ( (Disj x e. A B /\ ( X e. A /\ Y e. A ) /\ X =/= Y ) -> ( C i^i D ) = (/) )
Theorem	invdisj 4107*	If there is a function C ( y ) such that C ( y ) = x for all y e. B ( x ), then the sets B ( x ) for distinct x e. A are disjoint. (Contributed by Mario Carneiro, 10-Dec-2016.)
|- ( A. x e. A A. y e. B C = x -> Disj x e. A B )
Theorem	invdisjrab 4108*	The restricted class abstractions { x e. B | C = y } for distinct y e. A are disjoint. (Contributed by AV, 6-May-2020.) (Proof shortened by GG, 26-Jan-2024.)
|- Disj y e. A { x e. B | C = y }
Theorem	disjiun 4109*	A disjoint collection yields disjoint indexed unions for disjoint index sets. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Mario Carneiro, 14-Nov-2016.)
|- ( (Disj x e. A B /\ ( C C_ A /\ D C_ A /\ ( C i^i D ) = (/) ) ) -> ( U_ x e. C B i^i U_ x e. D B ) = (/) )
Theorem	sndisj 4110	Any collection of singletons is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- Disj x e. A { x }
Theorem	0disj 4111	Any collection of empty sets is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- Disj x e. A (/)
Theorem	disjxsn 4112*	A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- Disj x e. { A } B
Theorem	disjx0 4113	An empty collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- Disj x e. (/) B
2.1.22  Binary relations
Syntax	wbr 4114	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 4115	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 5031). (Contributed by NM, 31-Dec-1993.)
|- ( A R B <-> <. A , B >. e. R )
Theorem	breq 4116	Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.)
|- ( R = S -> ( A R B <-> A S B ) )
Theorem	breq1 4117	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
|- ( A = B -> ( A R C <-> B R C ) )
Theorem	breq2 4118	Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
|- ( A = B -> ( C R A <-> C R B ) )
Theorem	breq12 4119	Equality theorem for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )
Theorem	breqi 4120	Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)
|- R = S   =>    |- ( A R B <-> A S B )
Theorem	breq1i 4121	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- A = B   =>    |- ( A R C <-> B R C )
Theorem	breq2i 4122	Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- A = B   =>    |- ( C R A <-> C R B )
Theorem	breq12i 4123	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 4124	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A R C <-> B R C ) )
Theorem	breqd 4125	Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C A D <-> C B D ) )
Theorem	breq2d 4126	Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C R A <-> C R B ) )
Theorem	breq12d 4127	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 4128	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 4129	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 4130	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 4131	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 4132	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 4133	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 4134	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 4135	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- B R C   =>    |- A R C
Theorem	eqbrtrd 4136	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 4137	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- A = B   &    |- A R C   =>    |- B R C
Theorem	eqbrtrrd 4138	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 4139	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- A R B   &    |- B = C   =>    |- A R C
Theorem	breqtrd 4140	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 4141	Substitution of equal classes into a binary relation. (Contributed by NM, 5-Aug-1993.)
|- A R B   &    |- C = B   =>    |- A R C
Theorem	breqtrrd 4142	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 4143	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 4144	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 4145	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 4146	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 4147	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 4148	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 4149	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 4150	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 4151	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 4152	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 4153	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 4154	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 4155	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 4156	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 4157	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	ssbr 4158	Implication from a subclass relationship of binary relations. (Contributed by Peter Mazsa, 11-Nov-2019.)
|- ( A C_ B -> ( C A D -> C B D ) )
Theorem	ssbri 4159	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 4160	Deduction version of bound-variable hypothesis builder nfbr 4161. (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 4161	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 4162*	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 4163	The empty binary relation never holds. (Contributed by NM, 23-Aug-2018.)
|- -. A (/) B
Theorem	brne0 4164	If two sets are in a binary relation, the relation cannot be empty. In fact, the relation is also inhabited, as seen at brm 4165. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
|- ( A R B -> R =/= (/) )
Theorem	brm 4165*	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 4166	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 4167	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 4168	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 4169	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 4170*	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 4171*	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 4172*	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 4173*	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 4174*	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 4175	Extend class notation to include ordered-pair class abstraction (class builder).
class { <. x , y >. | ph }
Syntax	cmpt 4176	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 4177*	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 4178*	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 4179*	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 4180	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 4181*	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 4182	Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)
|- ( ph <-> ps )   =>    |- { <. x , y >. | ph } = { <. x , y >. | ps }
Theorem	nfopab 4183*	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 4184	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 4185	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 4186*	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 4187*	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 4188*	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 4189*	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 4190*	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 4191*	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 4192*	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 4193*	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 4194	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 4195	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 4196*	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 4197*	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 4198*	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 4199*	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 4200*	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 ) )