P. 65 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6401-6500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oa0 6401	Addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A e. On -> ( A +o (/) ) = A )
Theorem	om0 6402	Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A e. On -> ( A .o (/) ) = (/) )
Theorem	oei0 6403	Ordinal exponentiation with zero exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A e. On -> ( A ↑o (/) ) = 1o )
Theorem	oacl 6404	Closure law for ordinal addition. Proposition 8.2 of [TakeutiZaring] p. 57. (Contributed by NM, 5-May-1995.) (Constructive proof by Jim Kingdon, 26-Jul-2019.)
|- ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
Theorem	omcl 6405	Closure law for ordinal multiplication. Proposition 8.16 of [TakeutiZaring] p. 57. (Contributed by NM, 3-Aug-2004.) (Constructive proof by Jim Kingdon, 26-Jul-2019.)
|- ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )
Theorem	oeicl 6406	Closure law for ordinal exponentiation. (Contributed by Jim Kingdon, 26-Jul-2019.)
|- ( ( A e. On /\ B e. On ) -> ( A ↑o B ) e. On )
Theorem	oav2 6407*	Value of ordinal addition. (Contributed by Mario Carneiro and Jim Kingdon, 12-Aug-2019.)
|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = ( A u. U_ x e. B suc ( A +o x ) ) )
Theorem	oasuc 6408	Addition with successor. Definition 8.1 of [TakeutiZaring] p. 56. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A +o suc B ) = suc ( A +o B ) )
Theorem	omv2 6409*	Value of ordinal multiplication. (Contributed by Jim Kingdon, 23-Aug-2019.)
|- ( ( A e. On /\ B e. On ) -> ( A .o B ) = U_ x e. B ( ( A .o x ) +o A ) )
Theorem	onasuc 6410	Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( ( A e. On /\ B e. om ) -> ( A +o suc B ) = suc ( A +o B ) )
Theorem	oa1suc 6411	Addition with 1 is same as successor. Proposition 4.34(a) of [Mendelson] p. 266. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- ( A e. On -> ( A +o 1o ) = suc A )
Theorem	o1p1e2 6412	1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.)
|- ( 1o +o 1o ) = 2o
Theorem	oawordi 6413	Weak ordering property of ordinal addition. (Contributed by Jim Kingdon, 27-Jul-2019.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( C +o A ) C_ ( C +o B ) ) )
Theorem	oawordriexmid 6414*	A weak ordering property of ordinal addition which implies excluded middle. The property is proposition 8.7 of [TakeutiZaring] p. 59. Compare with oawordi 6413. (Contributed by Jim Kingdon, 15-May-2022.)
|- ( ( a e. On /\ b e. On /\ c e. On ) -> ( a C_ b -> ( a +o c ) C_ ( b +o c ) ) )   =>    |- ( ph \/ -. ph )
Theorem	oaword1 6415	An ordinal is less than or equal to its sum with another. Part of Exercise 5 of [TakeutiZaring] p. 62. (Contributed by NM, 6-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> A C_ ( A +o B ) )
Theorem	omsuc 6416	Multiplication with successor. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
Theorem	onmsuc 6417	Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. On /\ B e. om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
2.6.24  Natural number arithmetic
Theorem	nna0 6418	Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.)
|- ( A e. om -> ( A +o (/) ) = A )
Theorem	nnm0 6419	Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.)
|- ( A e. om -> ( A .o (/) ) = (/) )
Theorem	nnasuc 6420	Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A +o suc B ) = suc ( A +o B ) )
Theorem	nnmsuc 6421	Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
Theorem	nna0r 6422	Addition to zero. Remark in proof of Theorem 4K(2) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( A e. om -> ( (/) +o A ) = A )
Theorem	nnm0r 6423	Multiplication with zero. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( A e. om -> ( (/) .o A ) = (/) )
Theorem	nnacl 6424	Closure of addition of natural numbers. Proposition 8.9 of [TakeutiZaring] p. 59. (Contributed by NM, 20-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( A +o B ) e. om )
Theorem	nnmcl 6425	Closure of multiplication of natural numbers. Proposition 8.17 of [TakeutiZaring] p. 63. (Contributed by NM, 20-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( A .o B ) e. om )
Theorem	nnacli 6426	om is closed under addition. Inference form of nnacl 6424. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &    |- B e. om   =>    |- ( A +o B ) e. om
Theorem	nnmcli 6427	om is closed under multiplication. Inference form of nnmcl 6425. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &    |- B e. om   =>    |- ( A .o B ) e. om
Theorem	nnacom 6428	Addition of natural numbers is commutative. Theorem 4K(2) of [Enderton] p. 81. (Contributed by NM, 6-May-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A +o B ) = ( B +o A ) )
Theorem	nnaass 6429	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 6430	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 6431	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 6432	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 6433	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	nndir 6434	Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A +o B ) .o C ) = ( ( A .o C ) +o ( B .o C ) ) )
Theorem	nnsucelsuc 6435	Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucelsucr 4466, but the forward direction, for all ordinals, implies excluded middle as seen as onsucelsucexmid 4488. (Contributed by Jim Kingdon, 25-Aug-2019.)
|- ( B e. om -> ( A e. B <-> suc A e. suc B ) )
Theorem	nnsucsssuc 6436	Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4467, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4485. (Contributed by Jim Kingdon, 25-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> suc A C_ suc B ) )
Theorem	nntri3or 6437	Trichotomy for natural numbers. (Contributed by Jim Kingdon, 25-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> ( A e. B \/ A = B \/ B e. A ) )
Theorem	nntri2 6438	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
Theorem	nnsucuniel 6439	Given an element A of the union of a natural number B, suc A is an element of B itself. The reverse direction holds for all ordinals (sucunielr 4468). The forward direction for all ordinals implies excluded middle (ordsucunielexmid 4489). (Contributed by Jim Kingdon, 13-Mar-2022.)
|- ( B e. om -> ( A e. U. B <-> suc A e. B ) )
Theorem	nntri1 6440	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> -. B e. A ) )
Theorem	nntri3 6441	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-May-2020.)
|- ( ( A e. om /\ B e. om ) -> ( A = B <-> ( -. A e. B /\ -. B e. A ) ) )
Theorem	nntri2or2 6442	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-Sep-2021.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B \/ B C_ A ) )
Theorem	nndceq 6443	Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p. (varies). For the specific case where B is zero, see nndceq0 4576. (Contributed by Jim Kingdon, 31-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> DECID A = B )
Theorem	nndcel 6444	Set membership between two natural numbers is decidable. (Contributed by Jim Kingdon, 6-Sep-2019.)
|- ( ( A e. om /\ B e. om ) -> DECID A e. B )
Theorem	nnsseleq 6445	For natural numbers, inclusion is equivalent to membership or equality. (Contributed by Jim Kingdon, 16-Sep-2021.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
Theorem	nnsssuc 6446	A natural number is a subset of another natural number if and only if it belongs to its successor. (Contributed by Jim Kingdon, 22-Jul-2023.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> A e. suc B ) )
Theorem	nntr2 6447	Transitive law for natural numbers. (Contributed by Jim Kingdon, 22-Jul-2023.)
|- ( ( A e. om /\ C e. om ) -> ( ( A C_ B /\ B e. C ) -> A e. C ) )
Theorem	dcdifsnid 6448*	If we remove a single element from a set with decidable equality then put it back in, we end up with the original set. This strengthens difsnss 3702 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 17-Jun-2022.)
|- ( ( A. x e. A A. y e. A DECID x = y /\ B e. A ) -> ( ( A \ { B } ) u. { B } ) = A )
Theorem	fnsnsplitdc 6449*	Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015.) (Revised by Jim Kingdon, 29-Jan-2023.)
|- ( ( A. x e. A A. y e. A DECID x = y /\ F Fn A /\ X e. A ) -> F = ( ( F |` ( A \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )
Theorem	funresdfunsndc 6450*	Restricting a function to a domain without one element of the domain of the function, and adding a pair of this element and the function value of the element results in the function itself, where equality is decidable. (Contributed by AV, 2-Dec-2018.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- ( ( A. x e. dom F A. y e. dom FDECID x = y /\ Fun F /\ X e. dom F ) -> ( ( F |` ( _V \ { X } ) ) u. { <. X , ( F ` X ) >. } ) = F )
Theorem	nndifsnid 6451	If we remove a single element from a natural number then put it back in, we end up with the original natural number. This strengthens difsnss 3702 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 31-Aug-2021.)
|- ( ( A e. om /\ B e. A ) -> ( ( A \ { B } ) u. { B } ) = A )
Theorem	nnaordi 6452	Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58, limited to natural numbers. (Contributed by NM, 3-Feb-1996.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( B e. om /\ C e. om ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
Theorem	nnaord 6453	Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58, limited to natural numbers, and its converse. (Contributed by NM, 7-Mar-1996.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A e. B <-> ( C +o A ) e. ( C +o B ) ) )
Theorem	nnaordr 6454	Ordering property of addition of natural numbers. (Contributed by NM, 9-Nov-2002.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A e. B <-> ( A +o C ) e. ( B +o C ) ) )
Theorem	nnaword 6455	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 6456	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 6457	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 6458	Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
|- ( ( A e. om /\ B e. om ) -> A C_ ( B +o A ) )
Theorem	nnawordi 6459	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	nnmordi 6460	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 6461	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 6462	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 6463	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	1onn 6464	One is a natural number. (Contributed by NM, 29-Oct-1995.)
|- 1o e. om
Theorem	2onn 6465	The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
|- 2o e. om
Theorem	3onn 6466	The ordinal 3 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 3o e. om
Theorem	4onn 6467	The ordinal 4 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 4o e. om
Theorem	nnm1 6468	Multiply an element of om by 1o. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( A .o 1o ) = A )
Theorem	nnm2 6469	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 6470	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	nnaordex 6471*	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	nnawordex 6472*	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	nnm00 6473	The product of two natural numbers is zero iff at least one of them is zero. (Contributed by Jim Kingdon, 11-Nov-2004.)
|- ( ( A e. om /\ B e. om ) -> ( ( A .o B ) = (/) <-> ( A = (/) \/ B = (/) ) ) )
2.6.25  Equivalence relations and classes
Syntax	wer 6474	Extend the definition of a wff to include the equivalence predicate.
wff R Er A
Syntax	cec 6475	Extend the definition of a class to include equivalence class.
class [ A ] R
Syntax	cqs 6476	Extend the definition of a class to include quotient set.
class ( A /. R )
Definition	df-er 6477	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 6478 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 6497, ersymb 6491, and ertr 6492. (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 6478*	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 6479	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 6478). 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 6480. (Contributed by NM, 23-Jul-1995.)
|- [ A ] R = ( R " { A } )
Theorem	dfec2 6480*	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 6481	An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995.)
|- ( R e. B -> [ A ] R e. _V )
Theorem	ecexr 6482	An inhabited 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 6483*	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 6484	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 6485	Equality theorem for equivalence predicate. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( A = B -> ( R Er A <-> R Er B ) )
Theorem	errel 6486	An equivalence relation is a relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> Rel R )
Theorem	erdm 6487	The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> dom R = A )
Theorem	ercl 6488	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 6489	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 6490	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 6491	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 6492	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 6493	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 6494	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 6495	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 6496	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 6497	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 6498	The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> `' R = R )
Theorem	errn 6499	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 6500	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 ) )