P. 69 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6801-6900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	erref 6801	An equivalence relation is reflexive on its field. Compare Theorem 3M of [Enderton] p. 56. (Contributed by Mario Carneiro, 6-May-2013.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> A e. X )   =>    |- ( ph -> A R A )
Theorem	ercnv 6802	The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> `' R = R )
Theorem	errn 6803	The range and domain of an equivalence relation are equal. (Contributed by Rodolfo Medina, 11-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> ran R = A )
Theorem	erssxp 6804	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 6805	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 6806	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 6807*	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 6808	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 6809*	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 6810*	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 6811*	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 6812*	Lemma for eqer 6813. (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 6813*	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 6814	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 6815	The empty set is an equivalence relation on the empty set. (Contributed by Mario Carneiro, 5-Sep-2015.)
|- (/) Er (/)
Theorem	eceq1 6816	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> [ A ] C = [ B ] C )
Theorem	eceq1d 6817	Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
|- ( ph -> A = B )   =>    |- ( ph -> [ A ] C = [ B ] C )
Theorem	eceq2 6818	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> [ C ] A = [ C ] B )
Theorem	eceq2i 6819	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 6820	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 6821	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 6822	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 6823	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 6824	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 6825*	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 6826	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 6827	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 6828	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 6829	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 6830	An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.)
|- [ A ] _I = { A }
Theorem	qseq1 6831	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> ( A /. C ) = ( B /. C ) )
Theorem	qseq2 6832	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> ( C /. A ) = ( C /. B ) )
Theorem	elqsg 6833*	Closed form of elqs 6834. (Contributed by Rodolfo Medina, 12-Oct-2010.)
|- ( B e. V -> ( B e. ( A /. R ) <-> E. x e. A B = [ x ] R ) )
Theorem	elqs 6834*	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 6835*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( B e. ( A /. R ) -> E. x e. A B = [ x ] R )
Theorem	ecelqsg 6836	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 6837	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 6838	"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 6839	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 6840	A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|- A e. _V   =>    |- ( A /. R ) e. _V
Theorem	uniqs 6841	The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|- ( R e. V -> U. ( A /. R ) = ( R " A ) )
Theorem	qsss 6842	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 6843	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 6844	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 6845	Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.)
|- R e. _V   =>    |- [ A ] R = U. ( { A } /. R )
Theorem	ecid 6846	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 6847	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 6848	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 6849*	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 6850*	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 6851*	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 6852	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 6853	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 6854	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 6855*	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 6856*	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 6857	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 6858	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 6859	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 6860	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 6861*	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 6862*	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 6863*	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 6864*	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 6865*	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 6866*	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 6867*	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 6868*	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 6869*	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 6870*	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 6871*	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 6872*	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 6873*	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 6874*	Lemma for eroprf 6876. (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 6875*	Lemma for eroprf 6876. (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 6876*	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 6877*	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 6878*	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 6879*	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 6880*	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 6881*	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 6882*	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 6883*	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 6884*	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 6885*	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 6886*	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 6887*	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 6888*	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 6889*	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 6890*	Lemma used to transfer a commutative law via an equivalence relation. Most uses will want ecovicom 6891 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 6891*	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 6892*	Lemma used to transfer an associative law via an equivalence relation. In most cases ecoviass 6893 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 6893*	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 6894*	Lemma used to transfer a distributive law via an equivalence relation. Most likely ecovidi 6895 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 6895*	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.27  The mapping operation
Syntax	cmap 6896	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 6897	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 6898*	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 6908). 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 6899*	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 6907). 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 6898) . See mapsspm 6930 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 6900*	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 } = (/) )