P. 78 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7701-7800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnawordi 7701	Adding to both sides of an inequality in om. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 12-May-2012.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B -> ( A +o C ) C_ ( B +o C ) ) )
Theorem	nnaass 7702	Addition of natural numbers is associative. Theorem 4K(1) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) )
Theorem	nndi 7703	Distributive law for natural numbers (left-distributivity). Theorem 4K(3) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) )
Theorem	nnmass 7704	Multiplication of natural numbers is associative. Theorem 4K(4) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) )
Theorem	nnmsucr 7705	Multiplication with successor. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( suc A .o B ) = ( ( A .o B ) +o B ) )
Theorem	nnmcom 7706	Multiplication of natural numbers is commutative. Theorem 4K(5) of [Enderton] p. 81. (Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( A .o B ) = ( B .o A ) )
Theorem	nnaword 7707	Weak ordering property of addition. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B <-> ( C +o A ) C_ ( C +o B ) ) )
Theorem	nnacan 7708	Cancellation law for addition of natural numbers. (Contributed by NM, 27-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A +o B ) = ( A +o C ) <-> B = C ) )
Theorem	nnaword1 7709	Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> A C_ ( A +o B ) )
Theorem	nnaword2 7710	Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
|- ( ( A e. om /\ B e. om ) -> A C_ ( B +o A ) )
Theorem	nnmordi 7711	Ordering property of multiplication. Half of Proposition 8.19 of [TakeutiZaring] p. 63, limited to natural numbers. (Contributed by NM, 18-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( ( B e. om /\ C e. om ) /\ (/) e. C ) -> ( A e. B -> ( C .o A ) e. ( C .o B ) ) )
Theorem	nnmord 7712	Ordering property of multiplication. Proposition 8.19 of [TakeutiZaring] p. 63, limited to natural numbers. (Contributed by NM, 22-Jan-1996.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A e. B /\ (/) e. C ) <-> ( C .o A ) e. ( C .o B ) ) )
Theorem	nnmword 7713	Weak ordering property of ordinal multiplication. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( ( ( A e. om /\ B e. om /\ C e. om ) /\ (/) e. C ) -> ( A C_ B <-> ( C .o A ) C_ ( C .o B ) ) )
Theorem	nnmcan 7714	Cancellation law for multiplication of natural numbers. (Contributed by NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( ( A e. om /\ B e. om /\ C e. om ) /\ (/) e. A ) -> ( ( A .o B ) = ( A .o C ) <-> B = C ) )
Theorem	nnmwordi 7715	Weak ordering property of multiplication. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B -> ( C .o A ) C_ ( C .o B ) ) )
Theorem	nnmwordri 7716	Weak ordering property of ordinal multiplication. Proposition 8.21 of [TakeutiZaring] p. 63, limited to natural numbers. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B -> ( A .o C ) C_ ( B .o C ) ) )
Theorem	nnawordex 7717*	Equivalence for weak ordering of natural numbers. (Contributed by NM, 8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> E. x e. om ( A +o x ) = B ) )
Theorem	nnaordex 7718*	Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88. (Contributed by NM, 5-Dec-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A e. B <-> E. x e. om ( (/) e. x /\ ( A +o x ) = B ) ) )
Theorem	1onn 7719	One is a natural number. (Contributed by NM, 29-Oct-1995.)
|- 1o e. om
Theorem	2onn 7720	The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
|- 2o e. om
Theorem	3onn 7721	The ordinal 3 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 3o e. om
Theorem	4onn 7722	The ordinal 4 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 4o e. om
Theorem	oaabslem 7723	Lemma for oaabs 7724. (Contributed by NM, 9-Dec-2004.)
|- ( ( om e. On /\ A e. om ) -> ( A +o om ) = om )
Theorem	oaabs 7724	Ordinal addition absorbs a natural number added to the left of a transfinite number. Proposition 8.10 of [TakeutiZaring] p. 59. (Contributed by NM, 9-Dec-2004.) (Proof shortened by Mario Carneiro, 29-May-2015.)
|- ( ( ( A e. om /\ B e. On ) /\ om C_ B ) -> ( A +o B ) = B )
Theorem	oaabs2 7725	The absorption law oaabs 7724 is also a property of higher powers of om. (Contributed by Mario Carneiro, 29-May-2015.)
|- ( ( ( A e. ( om ^o C ) /\ B e. On ) /\ ( om ^o C ) C_ B ) -> ( A +o B ) = B )
Theorem	omabslem 7726	Lemma for omabs 7727. (Contributed by Mario Carneiro, 30-May-2015.)
|- ( ( om e. On /\ A e. om /\ (/) e. A ) -> ( A .o om ) = om )
Theorem	omabs 7727	Ordinal multiplication is also absorbed by powers of om. (Contributed by Mario Carneiro, 30-May-2015.)
|- ( ( ( A e. om /\ (/) e. A ) /\ ( B e. On /\ (/) e. B ) ) -> ( A .o ( om ^o B ) ) = ( om ^o B ) )
Theorem	nnm1 7728	Multiply an element of om by 1o. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( A .o 1o ) = A )
Theorem	nnm2 7729	Multiply an element of om by 2o. (Contributed by Scott Fenton, 18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( A .o 2o ) = ( A +o A ) )
Theorem	nn2m 7730	Multiply an element of om by 2o. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( 2o .o A ) = ( A +o A ) )
Theorem	nnneo 7731	If a natural number is even, its successor is odd. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C = ( 2o .o A ) ) -> -. suc C = ( 2o .o B ) )
Theorem	nneob 7732*	A natural number is even iff its successor is odd. (Contributed by NM, 26-Jan-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( A e. om -> ( E. x e. om A = ( 2o .o x ) <-> -. E. x e. om suc A = ( 2o .o x ) ) )
Theorem	omsmolem 7733*	Lemma for omsmo 7734. (Contributed by NM, 30-Nov-2003.) (Revised by David Abernethy, 1-Jan-2014.)
|- ( y e. om -> ( ( ( A C_ On /\ F : om --> A ) /\ A. x e. om ( F ` x ) e. ( F ` suc x ) ) -> ( z e. y -> ( F ` z ) e. ( F ` y ) ) ) )
Theorem	omsmo 7734*	A strictly monotonic ordinal function on the set of natural numbers is one-to-one. (Contributed by NM, 30-Nov-2003.) (Revised by David Abernethy, 1-Jan-2014.)
|- ( ( ( A C_ On /\ F : om --> A ) /\ A. x e. om ( F ` x ) e. ( F ` suc x ) ) -> F : om -1-1-> A )
Theorem	omopthlem1 7735	Lemma for omopthi 7737. (Contributed by Scott Fenton, 18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- A e. om   &    |- C e. om   =>    |- ( A e. C -> ( ( A .o A ) +o ( A .o 2o ) ) e. ( C .o C ) )
Theorem	omopthlem2 7736	Lemma for omopthi 7737. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- A e. om   &    |- B e. om   &    |- C e. om   &    |- D e. om   =>    |- ( ( A +o B ) e. C -> -. ( ( C .o C ) +o D ) = ( ( ( A +o B ) .o ( A +o B ) ) +o B ) )
Theorem	omopthi 7737	An ordered pair theorem for om. Theorem 17.3 of [Quine] p. 124. This proof is adapted from nn0opthi 13057. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- A e. om   &    |- B e. om   &    |- C e. om   &    |- D e. om   =>    |- ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( A = C /\ B = D ) )
Theorem	omopth 7738	An ordered pair theorem for finite integers. Analogous to nn0opthi 13057. (Contributed by Scott Fenton, 1-May-2012.)
|- ( ( ( A e. om /\ B e. om ) /\ ( C e. om /\ D e. om ) ) -> ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( A = C /\ B = D ) ) )
2.4.20  Equivalence relations and classes
Syntax	wer 7739	Extend the definition of a wff to include the equivalence predicate.
wff R Er A
Syntax	cec 7740	Extend the definition of a class to include equivalence class.
class [ A ] R
Syntax	cqs 7741	Extend the definition of a class to include quotient set.
class ( A /. R )
Definition	df-er 7742	Define the equivalence relation predicate. Our notation is not standard. A formal notation doesn't seem to exist in the literature; instead only informal English tends to be used. The present definition, although somewhat cryptic, nicely avoids dummy variables. In dfer2 7743 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 7762, ersymb 7756, and ertr 7757. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 2-Nov-2015.)
|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
Theorem	dfer2 7743*	Alternate definition of equivalence predicate. (Contributed by NM, 3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A <-> ( Rel R /\ dom R = A /\ A. x A. y A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
Definition	df-ec 7744	Define the R-coset of A. Exercise 35 of [Enderton] p. 61. This is called the equivalence class of A modulo R when R is an equivalence relation (i.e. when Er R; see dfer2 7743). In this case, A is a representative (member) of the equivalence class [ A ] R, which contains all sets that are equivalent to A. Definition of [Enderton] p. 57 uses the notation [ A ] (subscript) R, although we simply follow the brackets by R since we don't have subscripted expressions. For an alternate definition, see dfec2 7745. (Contributed by NM, 23-Jul-1995.)
|- [ A ] R = ( R " { A } )
Theorem	dfec2 7745*	Alternate definition of R-coset of A. Definition 34 of [Suppes] p. 81. (Contributed by NM, 3-Jan-1997.) (Proof shortened by Mario Carneiro, 9-Jul-2014.)
|- ( A e. V -> [ A ] R = { y | A R y } )
Theorem	ecexg 7746	An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995.)
|- ( R e. B -> [ A ] R e. _V )
Theorem	ecexr 7747	A nonempty equivalence class implies the representative is a set. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( A e. [ B ] R -> B e. _V )
Definition	df-qs 7748*	Define quotient set. R is usually an equivalence relation. Definition of [Enderton] p. 58. (Contributed by NM, 23-Jul-1995.)
|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
Theorem	ereq1 7749	Equality theorem for equivalence predicate. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( R = S -> ( R Er A <-> S Er A ) )
Theorem	ereq2 7750	Equality theorem for equivalence predicate. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( A = B -> ( R Er A <-> R Er B ) )
Theorem	errel 7751	An equivalence relation is a relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> Rel R )
Theorem	erdm 7752	The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> dom R = A )
Theorem	ercl 7753	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   =>    |- ( ph -> A e. X )
Theorem	ersym 7754	An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   =>    |- ( ph -> B R A )
Theorem	ercl2 7755	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   =>    |- ( ph -> B e. X )
Theorem	ersymb 7756	An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   =>    |- ( ph -> ( A R B <-> B R A ) )
Theorem	ertr 7757	An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   =>    |- ( ph -> ( ( A R B /\ B R C ) -> A R C ) )
Theorem	ertrd 7758	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	ertr2d 7759	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   &    |- ( ph -> B R C )   =>    |- ( ph -> C R A )
Theorem	ertr3d 7760	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> B R A )   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	ertr4d 7761	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   &    |- ( ph -> C R B )   =>    |- ( ph -> A R C )
Theorem	erref 7762	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 7763	The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> `' R = R )
Theorem	errn 7764	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 7765	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 7766	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 7767	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 7768*	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	iseri 7769*	A reflexive, symmetric, transitive relation is an equivalence relation on its domain. Inference version of iserd 7768, which avoids the need to provide a "dummy antecedent" ph if there is no natural one to choose. (Contributed by AV, 30-Apr-2021.)
|- Rel R   &    |- ( x R y -> y R x )   &    |- ( ( x R y /\ y R z ) -> x R z )   &    |- ( x e. A <-> x R x )   =>    |- R Er A
Theorem	iseriALT 7770*	Alternate proof of iseri 7769, avoiding the usage of trud 1493 and T. as antecedent by using ax-mp 5 and one of the hypotheses as antecedent. This results, however, in a slightly longer proof. (Contributed by AV, 30-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
|- Rel R   &    |- ( x R y -> y R x )   &    |- ( ( x R y /\ y R z ) -> x R z )   &    |- ( x e. A <-> x R x )   =>    |- R Er A
Theorem	brdifun 7771	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 7772*	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 7773*	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 7774*	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	swoso 7775*	If the incomparability relation is equivalent to equality in a subset, then the partial order strictly orders the subset. (Contributed by Mario Carneiro, 30-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 -> Y C_ X )   &    |- ( ( ph /\ ( x e. Y /\ y e. Y /\ x R y ) ) -> x = y )   =>    |- ( ph -> .< Or Y )
Theorem	eqerlem 7776*	Lemma for eqer 7777. (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 7777*	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.) (Proof shortened by AV, 1-May-2021.)
|- ( x = y -> A = B )   &    |- R = { <. x , y >. | A = B }   =>    |- R Er _V
Theorem	eqerOLD 7778*	Obsolete proof of eqer 7777 as of 1-May-2021. 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.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = y -> A = B )   &    |- R = { <. x , y >. | A = B }   =>    |- R Er _V
Theorem	ider 7779	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 7780	The empty set is an equivalence relation on the empty set. (Contributed by Mario Carneiro, 5-Sep-2015.) (Proof shortened by AV, 1-May-2021.)
|- (/) Er (/)
Theorem	0erOLD 7781	Obsolete proof of 0er 7780 as of 1-May-2021. The empty set is an equivalence relation on the empty set. (Contributed by Mario Carneiro, 5-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (/) Er (/)
Theorem	eceq1 7782	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> [ A ] C = [ B ] C )
Theorem	eceq1d 7783	Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
|- ( ph -> A = B )   =>    |- ( ph -> [ A ] C = [ B ] C )
Theorem	eceq2 7784	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> [ C ] A = [ C ] B )
Theorem	elecg 7785	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 7786	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 7787	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 7788	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	ecdmn0 7789	A representative of a nonempty equivalence class belongs to the domain of the equivalence relation. (Contributed by NM, 15-Feb-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( A e. dom R <-> [ A ] R =/= (/) )
Theorem	ereldm 7790	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 7791	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 7792	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 7793	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	erdisj 7794	Equivalence classes do not overlap. In other words, two equivalence classes are either equal or disjoint. Theorem 74 of [Suppes] p. 83. (Contributed by NM, 15-Jun-2004.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( R Er X -> ( [ A ] R = [ B ] R \/ ( [ A ] R i^i [ B ] R ) = (/) ) )
Theorem	ecidsn 7795	An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.)
|- [ A ] _I = { A }
Theorem	qseq1 7796	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> ( A /. C ) = ( B /. C ) )
Theorem	qseq2 7797	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> ( C /. A ) = ( C /. B ) )
Theorem	elqsg 7798*	Closed form of elqs 7799. (Contributed by Rodolfo Medina, 12-Oct-2010.)
|- ( B e. V -> ( B e. ( A /. R ) <-> E. x e. A B = [ x ] R ) )
Theorem	elqs 7799*	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 7800*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( B e. ( A /. R ) -> E. x e. A B = [ x ] R )