P. 68 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6701-6800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	erssxp 6701	An equivalence relation is a subset of the cartesian product of the field. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> R C_ ( A X. A ) )
Theorem	erex 6702	An equivalence relation is a set if its domain is a set. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> ( A e. V -> R e. _V ) )
Theorem	erexb 6703	An equivalence relation is a set if and only if its domain is a set. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> ( R e. _V <-> A e. _V ) )
Theorem	iserd 6704*	A reflexive, symmetric, transitive relation is an equivalence relation on its domain. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> Rel R )   &    |- ( ( ph /\ x R y ) -> y R x )   &    |- ( ( ph /\ ( x R y /\ y R z ) ) -> x R z )   &    |- ( ph -> ( x e. A <-> x R x ) )   =>    |- ( ph -> R Er A )
Theorem	brdifun 6705	Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- R = ( ( X X. X ) \ ( .< u. `' .< ) )   =>    |- ( ( A e. X /\ B e. X ) -> ( A R B <-> -. ( A .< B \/ B .< A ) ) )
Theorem	swoer 6706*	Incomparability under a strict weak partial order is an equivalence relation. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- R = ( ( X X. X ) \ ( .< u. `' .< ) )   &    |- ( ( ph /\ ( y e. X /\ z e. X ) ) -> ( y .< z -> -. z .< y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x .< y -> ( x .< z \/ z .< y ) ) )   =>    |- ( ph -> R Er X )
Theorem	swoord1 6707*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|- R = ( ( X X. X ) \ ( .< u. `' .< ) )   &    |- ( ( ph /\ ( y e. X /\ z e. X ) ) -> ( y .< z -> -. z .< y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x .< y -> ( x .< z \/ z .< y ) ) )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> A R B )   =>    |- ( ph -> ( A .< C <-> B .< C ) )
Theorem	swoord2 6708*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|- R = ( ( X X. X ) \ ( .< u. `' .< ) )   &    |- ( ( ph /\ ( y e. X /\ z e. X ) ) -> ( y .< z -> -. z .< y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x .< y -> ( x .< z \/ z .< y ) ) )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> A R B )   =>    |- ( ph -> ( C .< A <-> C .< B ) )
Theorem	eqerlem 6709*	Lemma for eqer 6710. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
|- ( x = y -> A = B )   &    |- R = { <. x , y >. | A = B }   =>    |- ( z R w <-> [_ z / x ]_ A = [_ w / x ]_ A )
Theorem	eqer 6710*	Equivalence relation involving equality of dependent classes A ( x ) and B ( y ). (Contributed by NM, 17-Mar-2008.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( x = y -> A = B )   &    |- R = { <. x , y >. | A = B }   =>    |- R Er _V
Theorem	ider 6711	The identity relation is an equivalence relation. (Contributed by NM, 10-May-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof shortened by Mario Carneiro, 9-Jul-2014.)
|- _I Er _V
Theorem	0er 6712	The empty set is an equivalence relation on the empty set. (Contributed by Mario Carneiro, 5-Sep-2015.)
|- (/) Er (/)
Theorem	eceq1 6713	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> [ A ] C = [ B ] C )
Theorem	eceq1d 6714	Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
|- ( ph -> A = B )   =>    |- ( ph -> [ A ] C = [ B ] C )
Theorem	eceq2 6715	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> [ C ] A = [ C ] B )
Theorem	eceq2i 6716	Equality theorem for the A-coset and B-coset of C, inference version. (Contributed by Peter Mazsa, 11-May-2021.)
|- A = B   =>    |- [ C ] A = [ C ] B
Theorem	eceq2d 6717	Equality theorem for the A-coset and B-coset of C, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.)
|- ( ph -> A = B )   =>    |- ( ph -> [ C ] A = [ C ] B )
Theorem	elecg 6718	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ( A e. V /\ B e. W ) -> ( A e. [ B ] R <-> B R A ) )
Theorem	elec 6719	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.)
|- A e. _V   &    |- B e. _V   =>    |- ( A e. [ B ] R <-> B R A )
Theorem	relelec 6720	Membership in an equivalence class when R is a relation. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( Rel R -> ( A e. [ B ] R <-> B R A ) )
Theorem	ecss 6721	An equivalence class is a subset of the domain. (Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   =>    |- ( ph -> [ A ] R C_ X )
Theorem	ecdmn0m 6722*	A representative of an inhabited equivalence class belongs to the domain of the equivalence relation. (Contributed by Jim Kingdon, 21-Aug-2019.)
|- ( A e. dom R <-> E. x x e. [ A ] R )
Theorem	ereldm 6723	Equality of equivalence classes implies equivalence of domain membership. (Contributed by NM, 28-Jan-1996.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> [ A ] R = [ B ] R )   =>    |- ( ph -> ( A e. X <-> B e. X ) )
Theorem	erth 6724	Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> A e. X )   =>    |- ( ph -> ( A R B <-> [ A ] R = [ B ] R ) )
Theorem	erth2 6725	Basic property of equivalence relations. Compare Theorem 73 of [Suppes] p. 82. Assumes membership of the second argument in the domain. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> B e. X )   =>    |- ( ph -> ( A R B <-> [ A ] R = [ B ] R ) )
Theorem	erthi 6726	Basic property of equivalence relations. Part of Lemma 3N of [Enderton] p. 57. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   =>    |- ( ph -> [ A ] R = [ B ] R )
Theorem	ecidsn 6727	An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.)
|- [ A ] _I = { A }
Theorem	qseq1 6728	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> ( A /. C ) = ( B /. C ) )
Theorem	qseq2 6729	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> ( C /. A ) = ( C /. B ) )
Theorem	elqsg 6730*	Closed form of elqs 6731. (Contributed by Rodolfo Medina, 12-Oct-2010.)
|- ( B e. V -> ( B e. ( A /. R ) <-> E. x e. A B = [ x ] R ) )
Theorem	elqs 6731*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|- B e. _V   =>    |- ( B e. ( A /. R ) <-> E. x e. A B = [ x ] R )
Theorem	elqsi 6732*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( B e. ( A /. R ) -> E. x e. A B = [ x ] R )
Theorem	ecelqsg 6733	Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( ( R e. V /\ B e. A ) -> [ B ] R e. ( A /. R ) )
Theorem	ecelqsi 6734	Membership of an equivalence class in a quotient set. (Contributed by NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- R e. _V   =>    |- ( B e. A -> [ B ] R e. ( A /. R ) )
Theorem	ecopqsi 6735	"Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996.)
|- R e. _V   &    |- S = ( ( A X. A ) /. R )   =>    |- ( ( B e. A /\ C e. A ) -> [ <. B , C >. ] R e. S )
Theorem	qsexg 6736	A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( A e. V -> ( A /. R ) e. _V )
Theorem	qsex 6737	A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|- A e. _V   =>    |- ( A /. R ) e. _V
Theorem	uniqs 6738	The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|- ( R e. V -> U. ( A /. R ) = ( R " A ) )
Theorem	qsss 6739	A quotient set is a set of subsets of the base set. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er A )   =>    |- ( ph -> ( A /. R ) C_ ~P A )
Theorem	uniqs2 6740	The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- ( ph -> R Er A )   &    |- ( ph -> R e. V )   =>    |- ( ph -> U. ( A /. R ) = A )
Theorem	snec 6741	The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- A e. _V   =>    |- { [ A ] R } = ( { A } /. R )
Theorem	ecqs 6742	Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.)
|- R e. _V   =>    |- [ A ] R = U. ( { A } /. R )
Theorem	ecid 6743	A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- A e. _V   =>    |- [ A ] `' _E = A
Theorem	ecidg 6744	A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by Jim Kingdon, 8-Jan-2020.)
|- ( A e. V -> [ A ] `' _E = A )
Theorem	qsid 6745	A set is equal to its quotient set mod converse epsilon. (Note: converse epsilon is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( A /. `' _E ) = A
Theorem	ectocld 6746*	Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- S = ( B /. R )   &    |- ( [ x ] R = A -> ( ph <-> ps ) )   &    |- ( ( ch /\ x e. B ) -> ph )   =>    |- ( ( ch /\ A e. S ) -> ps )
Theorem	ectocl 6747*	Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- S = ( B /. R )   &    |- ( [ x ] R = A -> ( ph <-> ps ) )   &    |- ( x e. B -> ph )   =>    |- ( A e. S -> ps )
Theorem	elqsn0m 6748*	An element of a quotient set is inhabited. (Contributed by Jim Kingdon, 21-Aug-2019.)
|- ( ( dom R = A /\ B e. ( A /. R ) ) -> E. x x e. B )
Theorem	elqsn0 6749	A quotient set doesn't contain the empty set. (Contributed by NM, 24-Aug-1995.)
|- ( ( dom R = A /\ B e. ( A /. R ) ) -> B =/= (/) )
Theorem	ecelqsdm 6750	Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995.)
|- ( ( dom R = A /\ [ B ] R e. ( A /. R ) ) -> B e. A )
Theorem	xpider 6751	A square Cartesian product is an equivalence relation (in general it's not a poset). (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( A X. A ) Er A
Theorem	iinerm 6752*	The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( ( E. y y e. A /\ A. x e. A R Er B ) -> |^|_ x e. A R Er B )
Theorem	riinerm 6753*	The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( ( E. y y e. A /\ A. x e. A R Er B ) -> ( ( B X. B ) i^i |^|_ x e. A R ) Er B )
Theorem	erinxp 6754	A restricted equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er A )   &    |- ( ph -> B C_ A )   =>    |- ( ph -> ( R i^i ( B X. B ) ) Er B )
Theorem	ecinxp 6755	Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- ( ( ( R " A ) C_ A /\ B e. A ) -> [ B ] R = [ B ] ( R i^i ( A X. A ) ) )
Theorem	qsinxp 6756	Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ( R " A ) C_ A -> ( A /. R ) = ( A /. ( R i^i ( A X. A ) ) ) )
Theorem	qsel 6757	If an element of a quotient set contains a given element, it is equal to the equivalence class of the element. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( ( R Er X /\ B e. ( A /. R ) /\ C e. B ) -> B = [ C ] R )
Theorem	qliftlem 6758*	F, a function lift, is a subset of R X. S. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ( ph /\ x e. X ) -> [ x ] R e. ( X /. R ) )
Theorem	qliftrel 6759*	F, a function lift, is a subset of R X. S. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ph -> F C_ ( ( X /. R ) X. Y ) )
Theorem	qliftel 6760*	Elementhood in the relation F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ph -> ( [ C ] R F D <-> E. x e. X ( C R x /\ D = A ) ) )
Theorem	qliftel1 6761*	Elementhood in the relation F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ( ph /\ x e. X ) -> [ x ] R F A )
Theorem	qliftfun 6762*	The function F is the unique function defined by F ` [ x ] = A, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   &    |- ( x = y -> A = B )   =>    |- ( ph -> ( Fun F <-> A. x A. y ( x R y -> A = B ) ) )
Theorem	qliftfund 6763*	The function F is the unique function defined by F ` [ x ] = A, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   &    |- ( x = y -> A = B )   &    |- ( ( ph /\ x R y ) -> A = B )   =>    |- ( ph -> Fun F )
Theorem	qliftfuns 6764*	The function F is the unique function defined by F ` [ x ] = A, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ph -> ( Fun F <-> A. y A. z ( y R z -> [_ y / x ]_ A = [_ z / x ]_ A ) ) )
Theorem	qliftf 6765*	The domain and codomain of the function F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ph -> ( Fun F <-> F : ( X /. R ) --> Y ) )
Theorem	qliftval 6766*	The value of the function F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   &    |- ( x = C -> A = B )   &    |- ( ph -> Fun F )   =>    |- ( ( ph /\ C e. X ) -> ( F ` [ C ] R ) = B )
Theorem	ecoptocl 6767*	Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995.)
|- S = ( ( B X. C ) /. R )   &    |- ( [ <. x , y >. ] R = A -> ( ph <-> ps ) )   &    |- ( ( x e. B /\ y e. C ) -> ph )   =>    |- ( A e. S -> ps )
Theorem	2ecoptocl 6768*	Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995.)
|- S = ( ( C X. D ) /. R )   &    |- ( [ <. x , y >. ] R = A -> ( ph <-> ps ) )   &    |- ( [ <. z , w >. ] R = B -> ( ps <-> ch ) )   &    |- ( ( ( x e. C /\ y e. D ) /\ ( z e. C /\ w e. D ) ) -> ph )   =>    |- ( ( A e. S /\ B e. S ) -> ch )
Theorem	3ecoptocl 6769*	Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995.)
|- S = ( ( D X. D ) /. R )   &    |- ( [ <. x , y >. ] R = A -> ( ph <-> ps ) )   &    |- ( [ <. z , w >. ] R = B -> ( ps <-> ch ) )   &    |- ( [ <. v , u >. ] R = C -> ( ch <-> th ) )   &    |- ( ( ( x e. D /\ y e. D ) /\ ( z e. D /\ w e. D ) /\ ( v e. D /\ u e. D ) ) -> ph )   =>    |- ( ( A e. S /\ B e. S /\ C e. S ) -> th )
Theorem	brecop 6770*	Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.)
|- .~ e. _V   &    |- .~ Er ( G X. G )   &    |- H = ( ( G X. G ) /. .~ )   &    |- .<_ = { <. x , y >. | ( ( x e. H /\ y e. H ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] .~ /\ y = [ <. v , u >. ] .~ ) /\ ph ) ) }   &    |- ( ( ( ( z e. G /\ w e. G ) /\ ( A e. G /\ B e. G ) ) /\ ( ( v e. G /\ u e. G ) /\ ( C e. G /\ D e. G ) ) ) -> ( ( [ <. z , w >. ] .~ = [ <. A , B >. ] .~ /\ [ <. v , u >. ] .~ = [ <. C , D >. ] .~ ) -> ( ph <-> ps ) ) )   =>    |- ( ( ( A e. G /\ B e. G ) /\ ( C e. G /\ D e. G ) ) -> ( [ <. A , B >. ] .~ .<_ [ <. C , D >. ] .~ <-> ps ) )
Theorem	eroveu 6771*	Lemma for eroprf 6773. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- J = ( A /. R )   &    |- K = ( B /. S )   &    |- ( ph -> T e. Z )   &    |- ( ph -> R Er U )   &    |- ( ph -> S Er V )   &    |- ( ph -> T Er W )   &    |- ( ph -> A C_ U )   &    |- ( ph -> B C_ V )   &    |- ( ph -> C C_ W )   &    |- ( ph -> .+ : ( A X. B ) --> C )   &    |- ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( r R s /\ t S u ) -> ( r .+ t ) T ( s .+ u ) ) )   =>    |- ( ( ph /\ ( X e. J /\ Y e. K ) ) -> E! z E. p e. A E. q e. B ( ( X = [ p ] R /\ Y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )
Theorem	erovlem 6772*	Lemma for eroprf 6773. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- J = ( A /. R )   &    |- K = ( B /. S )   &    |- ( ph -> T e. Z )   &    |- ( ph -> R Er U )   &    |- ( ph -> S Er V )   &    |- ( ph -> T Er W )   &    |- ( ph -> A C_ U )   &    |- ( ph -> B C_ V )   &    |- ( ph -> C C_ W )   &    |- ( ph -> .+ : ( A X. B ) --> C )   &    |- ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( r R s /\ t S u ) -> ( r .+ t ) T ( s .+ u ) ) )   &    |- .+^ = { <. <. x , y >. , z >. | E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) }   =>    |- ( ph -> .+^ = ( x e. J , y e. K |-> ( iota z E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) ) )
Theorem	eroprf 6773*	Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- J = ( A /. R )   &    |- K = ( B /. S )   &    |- ( ph -> T e. Z )   &    |- ( ph -> R Er U )   &    |- ( ph -> S Er V )   &    |- ( ph -> T Er W )   &    |- ( ph -> A C_ U )   &    |- ( ph -> B C_ V )   &    |- ( ph -> C C_ W )   &    |- ( ph -> .+ : ( A X. B ) --> C )   &    |- ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( r R s /\ t S u ) -> ( r .+ t ) T ( s .+ u ) ) )   &    |- .+^ = { <. <. x , y >. , z >. | E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) }   &    |- ( ph -> R e. X )   &    |- ( ph -> S e. Y )   &    |- L = ( C /. T )   =>    |- ( ph -> .+^ : ( J X. K ) --> L )
Theorem	eroprf2 6774*	Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- J = ( A /. .~ )   &    |- .+^ = { <. <. x , y >. , z >. | E. p e. A E. q e. A ( ( x = [ p ] .~ /\ y = [ q ] .~ ) /\ z = [ ( p .+ q ) ] .~ ) }   &    |- ( ph -> .~ e. X )   &    |- ( ph -> .~ Er U )   &    |- ( ph -> A C_ U )   &    |- ( ph -> .+ : ( A X. A ) --> A )   &    |- ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. A /\ u e. A ) ) ) -> ( ( r .~ s /\ t .~ u ) -> ( r .+ t ) .~ ( s .+ u ) ) )   =>    |- ( ph -> .+^ : ( J X. J ) --> J )
Theorem	ecopoveq 6775*	This is the first of several theorems about equivalence relations of the kind used in construction of fractions and signed reals, involving operations on equivalent classes of ordered pairs. This theorem expresses the relation .~ (specified by the hypothesis) in terms of its operation F. (Contributed by NM, 16-Aug-1995.)
|- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .+ u ) = ( w .+ v ) ) ) }   =>    |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( <. A , B >. .~ <. C , D >. <-> ( A .+ D ) = ( B .+ C ) ) )
Theorem	ecopovsym 6776*	Assuming the operation F is commutative, show that the relation .~, specified by the first hypothesis, is symmetric. (Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .+ u ) = ( w .+ v ) ) ) }   &    |- ( x .+ y ) = ( y .+ x )   =>    |- ( A .~ B -> B .~ A )
Theorem	ecopovtrn 6777*	Assuming that operation F is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation .~, specified by the first hypothesis, is transitive. (Contributed by NM, 11-Feb-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .+ u ) = ( w .+ v ) ) ) }   &    |- ( x .+ y ) = ( y .+ x )   &    |- ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )   &    |- ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) )   &    |- ( ( x e. S /\ y e. S ) -> ( ( x .+ y ) = ( x .+ z ) -> y = z ) )   =>    |- ( ( A .~ B /\ B .~ C ) -> A .~ C )
Theorem	ecopover 6778*	Assuming that operation F is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation .~, specified by the first hypothesis, is an equivalence relation. (Contributed by NM, 16-Feb-1996.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .+ u ) = ( w .+ v ) ) ) }   &    |- ( x .+ y ) = ( y .+ x )   &    |- ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )   &    |- ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) )   &    |- ( ( x e. S /\ y e. S ) -> ( ( x .+ y ) = ( x .+ z ) -> y = z ) )   =>    |- .~ Er ( S X. S )
Theorem	ecopovsymg 6779*	Assuming the operation F is commutative, show that the relation .~, specified by the first hypothesis, is symmetric. (Contributed by Jim Kingdon, 1-Sep-2019.)
|- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .+ u ) = ( w .+ v ) ) ) }   &    |- ( ( x e. S /\ y e. S ) -> ( x .+ y ) = ( y .+ x ) )   =>    |- ( A .~ B -> B .~ A )
Theorem	ecopovtrng 6780*	Assuming that operation F is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation .~, specified by the first hypothesis, is transitive. (Contributed by Jim Kingdon, 1-Sep-2019.)
|- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .+ u ) = ( w .+ v ) ) ) }   &    |- ( ( x e. S /\ y e. S ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )   &    |- ( ( x e. S /\ y e. S /\ z e. S ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ( x e. S /\ y e. S /\ z e. S ) -> ( ( x .+ y ) = ( x .+ z ) -> y = z ) )   =>    |- ( ( A .~ B /\ B .~ C ) -> A .~ C )
Theorem	ecopoverg 6781*	Assuming that operation F is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation .~, specified by the first hypothesis, is an equivalence relation. (Contributed by Jim Kingdon, 1-Sep-2019.)
|- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .+ u ) = ( w .+ v ) ) ) }   &    |- ( ( x e. S /\ y e. S ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )   &    |- ( ( x e. S /\ y e. S /\ z e. S ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ( x e. S /\ y e. S /\ z e. S ) -> ( ( x .+ y ) = ( x .+ z ) -> y = z ) )   =>    |- .~ Er ( S X. S )
Theorem	th3qlem1 6782*	Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The third hypothesis is the compatibility assumption. (Contributed by NM, 3-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- .~ Er S   &    |- ( ( ( y e. S /\ w e. S ) /\ ( z e. S /\ v e. S ) ) -> ( ( y .~ w /\ z .~ v ) -> ( y .+ z ) .~ ( w .+ v ) ) )   =>    |- ( ( A e. ( S /. .~ ) /\ B e. ( S /. .~ ) ) -> E* x E. y E. z ( ( A = [ y ] .~ /\ B = [ z ] .~ ) /\ x = [ ( y .+ z ) ] .~ ) )
Theorem	th3qlem2 6783*	Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. The fourth hypothesis is the compatibility assumption. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- .~ e. _V   &    |- .~ Er ( S X. S )   &    |- ( ( ( ( w e. S /\ v e. S ) /\ ( u e. S /\ t e. S ) ) /\ ( ( s e. S /\ f e. S ) /\ ( g e. S /\ h e. S ) ) ) -> ( ( <. w , v >. .~ <. u , t >. /\ <. s , f >. .~ <. g , h >. ) -> ( <. w , v >. .+ <. s , f >. ) .~ ( <. u , t >. .+ <. g , h >. ) ) )   =>    |- ( ( A e. ( ( S X. S ) /. .~ ) /\ B e. ( ( S X. S ) /. .~ ) ) -> E* z E. w E. v E. u E. t ( ( A = [ <. w , v >. ] .~ /\ B = [ <. u , t >. ] .~ ) /\ z = [ ( <. w , v >. .+ <. u , t >. ) ] .~ ) )
Theorem	th3qcor 6784*	Corollary of Theorem 3Q of [Enderton] p. 60. (Contributed by NM, 12-Nov-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|- .~ e. _V   &    |- .~ Er ( S X. S )   &    |- ( ( ( ( w e. S /\ v e. S ) /\ ( u e. S /\ t e. S ) ) /\ ( ( s e. S /\ f e. S ) /\ ( g e. S /\ h e. S ) ) ) -> ( ( <. w , v >. .~ <. u , t >. /\ <. s , f >. .~ <. g , h >. ) -> ( <. w , v >. .+ <. s , f >. ) .~ ( <. u , t >. .+ <. g , h >. ) ) )   &    |- G = { <. <. x , y >. , z >. | ( ( x e. ( ( S X. S ) /. .~ ) /\ y e. ( ( S X. S ) /. .~ ) ) /\ E. w E. v E. u E. t ( ( x = [ <. w , v >. ] .~ /\ y = [ <. u , t >. ] .~ ) /\ z = [ ( <. w , v >. .+ <. u , t >. ) ] .~ ) ) }   =>    |- Fun G
Theorem	th3q 6785*	Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- .~ e. _V   &    |- .~ Er ( S X. S )   &    |- ( ( ( ( w e. S /\ v e. S ) /\ ( u e. S /\ t e. S ) ) /\ ( ( s e. S /\ f e. S ) /\ ( g e. S /\ h e. S ) ) ) -> ( ( <. w , v >. .~ <. u , t >. /\ <. s , f >. .~ <. g , h >. ) -> ( <. w , v >. .+ <. s , f >. ) .~ ( <. u , t >. .+ <. g , h >. ) ) )   &    |- G = { <. <. x , y >. , z >. | ( ( x e. ( ( S X. S ) /. .~ ) /\ y e. ( ( S X. S ) /. .~ ) ) /\ E. w E. v E. u E. t ( ( x = [ <. w , v >. ] .~ /\ y = [ <. u , t >. ] .~ ) /\ z = [ ( <. w , v >. .+ <. u , t >. ) ] .~ ) ) }   =>    |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( [ <. A , B >. ] .~ G [ <. C , D >. ] .~ ) = [ ( <. A , B >. .+ <. C , D >. ) ] .~ )
Theorem	oviec 6786*	Express an operation on equivalence classes of ordered pairs in terms of equivalence class of operations on ordered pairs. See iset.mm for additional comments describing the hypotheses. (Unnecessary distinct variable restrictions were removed by David Abernethy, 4-Jun-2013.) (Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro, 4-Jun-2013.)
|- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> H e. ( S X. S ) )   &    |- ( ( ( a e. S /\ b e. S ) /\ ( g e. S /\ h e. S ) ) -> K e. ( S X. S ) )   &    |- ( ( ( c e. S /\ d e. S ) /\ ( t e. S /\ s e. S ) ) -> L e. ( S X. S ) )   &    |- .~ e. _V   &    |- .~ Er ( S X. S )   &    |- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ph ) ) }   &    |- ( ( ( z = a /\ w = b ) /\ ( v = c /\ u = d ) ) -> ( ph <-> ps ) )   &    |- ( ( ( z = g /\ w = h ) /\ ( v = t /\ u = s ) ) -> ( ph <-> ch ) )   &    |- .+ = { <. <. x , y >. , z >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = J ) ) }   &    |- ( ( ( w = a /\ v = b ) /\ ( u = g /\ f = h ) ) -> J = K )   &    |- ( ( ( w = c /\ v = d ) /\ ( u = t /\ f = s ) ) -> J = L )   &    |- ( ( ( w = A /\ v = B ) /\ ( u = C /\ f = D ) ) -> J = H )   &    |- .+^ = { <. <. x , y >. , z >. | ( ( x e. Q /\ y e. Q ) /\ E. a E. b E. c E. d ( ( x = [ <. a , b >. ] .~ /\ y = [ <. c , d >. ] .~ ) /\ z = [ ( <. a , b >. .+ <. c , d >. ) ] .~ ) ) }   &    |- Q = ( ( S X. S ) /. .~ )   &    |- ( ( ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) /\ ( ( g e. S /\ h e. S ) /\ ( t e. S /\ s e. S ) ) ) -> ( ( ps /\ ch ) -> K .~ L ) )   =>    |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( [ <. A , B >. ] .~ .+^ [ <. C , D >. ] .~ ) = [ H ] .~ )
Theorem	ecovcom 6787*	Lemma used to transfer a commutative law via an equivalence relation. Most uses will want ecovicom 6788 instead. (Contributed by NM, 29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|- C = ( ( S X. S ) /. .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = [ <. D , G >. ] .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( x e. S /\ y e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. x , y >. ] .~ ) = [ <. H , J >. ] .~ )   &    |- D = H   &    |- G = J   =>    |- ( ( A e. C /\ B e. C ) -> ( A .+ B ) = ( B .+ A ) )
Theorem	ecovicom 6788*	Lemma used to transfer a commutative law via an equivalence relation. (Contributed by Jim Kingdon, 15-Sep-2019.)
|- C = ( ( S X. S ) /. .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = [ <. D , G >. ] .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( x e. S /\ y e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. x , y >. ] .~ ) = [ <. H , J >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> D = H )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> G = J )   =>    |- ( ( A e. C /\ B e. C ) -> ( A .+ B ) = ( B .+ A ) )
Theorem	ecovass 6789*	Lemma used to transfer an associative law via an equivalence relation. In most cases ecoviass 6790 will be more useful. (Contributed by NM, 31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|- D = ( ( S X. S ) /. .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = [ <. G , H >. ] .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. N , Q >. ] .~ )   &    |- ( ( ( G e. S /\ H e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. G , H >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. J , K >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( N e. S /\ Q e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. N , Q >. ] .~ ) = [ <. L , M >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( G e. S /\ H e. S ) )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( N e. S /\ Q e. S ) )   &    |- J = L   &    |- K = M   =>    |- ( ( A e. D /\ B e. D /\ C e. D ) -> ( ( A .+ B ) .+ C ) = ( A .+ ( B .+ C ) ) )
Theorem	ecoviass 6790*	Lemma used to transfer an associative law via an equivalence relation. (Contributed by Jim Kingdon, 16-Sep-2019.)
|- D = ( ( S X. S ) /. .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = [ <. G , H >. ] .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. N , Q >. ] .~ )   &    |- ( ( ( G e. S /\ H e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. G , H >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. J , K >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( N e. S /\ Q e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. N , Q >. ] .~ ) = [ <. L , M >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( G e. S /\ H e. S ) )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( N e. S /\ Q e. S ) )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> J = L )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> K = M )   =>    |- ( ( A e. D /\ B e. D /\ C e. D ) -> ( ( A .+ B ) .+ C ) = ( A .+ ( B .+ C ) ) )
Theorem	ecovdi 6791*	Lemma used to transfer a distributive law via an equivalence relation. Most likely ecovidi 6792 will be more helpful. (Contributed by NM, 2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|- D = ( ( S X. S ) /. .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. M , N >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( M e. S /\ N e. S ) ) -> ( [ <. x , y >. ] .~ .x. [ <. M , N >. ] .~ ) = [ <. H , J >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .x. [ <. z , w >. ] .~ ) = [ <. W , X >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. x , y >. ] .~ .x. [ <. v , u >. ] .~ ) = [ <. Y , Z >. ] .~ )   &    |- ( ( ( W e. S /\ X e. S ) /\ ( Y e. S /\ Z e. S ) ) -> ( [ <. W , X >. ] .~ .+ [ <. Y , Z >. ] .~ ) = [ <. K , L >. ] .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( M e. S /\ N e. S ) )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( W e. S /\ X e. S ) )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( v e. S /\ u e. S ) ) -> ( Y e. S /\ Z e. S ) )   &    |- H = K   &    |- J = L   =>    |- ( ( A e. D /\ B e. D /\ C e. D ) -> ( A .x. ( B .+ C ) ) = ( ( A .x. B ) .+ ( A .x. C ) ) )
Theorem	ecovidi 6792*	Lemma used to transfer a distributive law via an equivalence relation. (Contributed by Jim Kingdon, 17-Sep-2019.)
|- D = ( ( S X. S ) /. .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. M , N >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( M e. S /\ N e. S ) ) -> ( [ <. x , y >. ] .~ .x. [ <. M , N >. ] .~ ) = [ <. H , J >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .x. [ <. z , w >. ] .~ ) = [ <. W , X >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. x , y >. ] .~ .x. [ <. v , u >. ] .~ ) = [ <. Y , Z >. ] .~ )   &    |- ( ( ( W e. S /\ X e. S ) /\ ( Y e. S /\ Z e. S ) ) -> ( [ <. W , X >. ] .~ .+ [ <. Y , Z >. ] .~ ) = [ <. K , L >. ] .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( M e. S /\ N e. S ) )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( W e. S /\ X e. S ) )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( v e. S /\ u e. S ) ) -> ( Y e. S /\ Z e. S ) )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> H = K )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> J = L )   =>    |- ( ( A e. D /\ B e. D /\ C e. D ) -> ( A .x. ( B .+ C ) ) = ( ( A .x. B ) .+ ( A .x. C ) ) )
2.6.26  The mapping operation
Syntax	cmap 6793	Extend the definition of a class to include the mapping operation. (Read for A ^m B, "the set of all functions that map from B to A.)
class ^m
Syntax	cpm 6794	Extend the definition of a class to include the partial mapping operation. (Read for A ^pm B, "the set of all partial functions that map from B to A.)
class ^pm
Definition	df-map 6795*	Define the mapping operation or set exponentiation. The set of all functions that map from B to A is written ( A ^m B ) (see mapval 6805). Many authors write A followed by B as a superscript for this operation and rely on context to avoid confusion other exponentiation operations (e.g., Definition 10.42 of [TakeutiZaring] p. 95). Other authors show B as a prefixed superscript, which is read " A pre B " (e.g., definition of [Enderton] p. 52). Definition 8.21 of [Eisenberg] p. 125 uses the notation Map( B, A) for our ( A ^m B ). The up-arrow is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976). We adopt the first case of his notation (simple exponentiation) and subscript it with m to distinguish it from other kinds of exponentiation. (Contributed by NM, 8-Dec-2003.)
|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
Definition	df-pm 6796*	Define the partial mapping operation. A partial function from B to A is a function from a subset of B to A. The set of all partial functions from B to A is written ( A ^pm B ) (see pmvalg 6804). A notation for this operation apparently does not appear in the literature. We use ^pm to distinguish it from the less general set exponentiation operation ^m (df-map 6795) . See mapsspm 6827 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.)
|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
Theorem	mapprc 6797*	When A is a proper class, the class of all functions mapping A to B is empty. Exercise 4.41 of [Mendelson] p. 255. (Contributed by NM, 8-Dec-2003.)
|- ( -. A e. _V -> { f | f : A --> B } = (/) )
Theorem	pmex 6798*	The class of all partial functions from one set to another is a set. (Contributed by NM, 15-Nov-2007.)
|- ( ( A e. C /\ B e. D ) -> { f | ( Fun f /\ f C_ ( A X. B ) ) } e. _V )
Theorem	mapex 6799*	The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of [Kunen] p. 31. (Contributed by Raph Levien, 4-Dec-2003.)
|- ( ( A e. C /\ B e. D ) -> { f | f : A --> B } e. _V )
Theorem	fnmap 6800	Set exponentiation has a universal domain. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ^m Fn ( _V X. _V )