P. 66 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6501-6600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sucinc2 6501*	Successor is increasing. (Contributed by Jim Kingdon, 14-Jul-2019.)
|- F = ( z e. _V |-> suc z )   =>    |- ( ( B e. On /\ A e. B ) -> ( F ` A ) C_ ( F ` B ) )
Theorem	fnoa 6502	Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Mario Carneiro, 3-Jul-2019.)
|- +o Fn ( On X. On )
Theorem	oaexg 6503	Ordinal addition is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- ( ( A e. V /\ B e. W ) -> ( A +o B ) e. _V )
Theorem	omfnex 6504*	The characteristic function for ordinal multiplication is defined everywhere. (Contributed by Jim Kingdon, 23-Aug-2019.)
|- ( A e. V -> ( x e. _V |-> ( x +o A ) ) Fn _V )
Theorem	fnom 6505	Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 3-Jul-2019.)
|- .o Fn ( On X. On )
Theorem	omexg 6506	Ordinal multiplication is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- ( ( A e. V /\ B e. W ) -> ( A .o B ) e. _V )
Theorem	fnoei 6507	Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.) (Revised by Mario Carneiro, 3-Jul-2019.)
|- ↑o Fn ( On X. On )
Theorem	oeiexg 6508	Ordinal exponentiation is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- ( ( A e. V /\ B e. W ) -> ( A ↑o B ) e. _V )
Theorem	oav 6509*	Value of ordinal addition. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = ( rec ( ( x e. _V |-> suc x ) , A ) ` B ) )
Theorem	omv 6510*	Value of ordinal multiplication. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ( A e. On /\ B e. On ) -> ( A .o B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) )
Theorem	oeiv 6511*	Value of ordinal exponentiation. (Contributed by Jim Kingdon, 9-Jul-2019.)
|- ( ( A e. On /\ B e. On ) -> ( A ↑o B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) )
Theorem	oa0 6512	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 6513	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 6514	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 6515	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 6516	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 6517	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 6518*	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 6519	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 6520*	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 6521	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 6522	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 6523	1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.)
|- ( 1o +o 1o ) = 2o
Theorem	oawordi 6524	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 6525*	A weak ordering property of ordinal addition which implies excluded middle. The property is proposition 8.7 of [TakeutiZaring] p. 59. Compare with oawordi 6524. (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 6526	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 6527	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 6528	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 6529	Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.)
|- ( A e. om -> ( A +o (/) ) = A )
Theorem	nnm0 6530	Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.)
|- ( A e. om -> ( A .o (/) ) = (/) )
Theorem	nnasuc 6531	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 6532	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 6533	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 6534	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 6535	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 6536	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 6537	om is closed under addition. Inference form of nnacl 6535. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &    |- B e. om   =>    |- ( A +o B ) e. om
Theorem	nnmcli 6538	om is closed under multiplication. Inference form of nnmcl 6536. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &    |- B e. om   =>    |- ( A .o B ) e. om
Theorem	nnacom 6539	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 6540	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 6541	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 6542	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 6543	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 6544	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 6545	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 6546	Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucelsucr 4541, but the forward direction, for all ordinals, implies excluded middle as seen as onsucelsucexmid 4563. (Contributed by Jim Kingdon, 25-Aug-2019.)
|- ( B e. om -> ( A e. B <-> suc A e. suc B ) )
Theorem	nnsucsssuc 6547	Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4542, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4560. (Contributed by Jim Kingdon, 25-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> suc A C_ suc B ) )
Theorem	nntri3or 6548	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 6549	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 6550	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 4543). The forward direction for all ordinals implies excluded middle (ordsucunielexmid 4564). (Contributed by Jim Kingdon, 13-Mar-2022.)
|- ( B e. om -> ( A e. U. B <-> suc A e. B ) )
Theorem	nntri1 6551	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 6552	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 6553	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 6554	Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p. (varies). For the specific case where B is zero, see nndceq0 4651. (Contributed by Jim Kingdon, 31-Aug-2019.)
|- ( ( A e. om /\ B e. om ) -> DECID A = B )
Theorem	nndcel 6555	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 6556	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 6557	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 6558	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 6559*	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 3765 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 6560*	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 6561*	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 6562	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 3765 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 6563	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 6564	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 6565	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 6566	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 6567	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 6568	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 6569	Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
|- ( ( A e. om /\ B e. om ) -> A C_ ( B +o A ) )
Theorem	nnawordi 6570	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 6571	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 6572	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 6573	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 6574	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 6575	One is a natural number. (Contributed by NM, 29-Oct-1995.)
|- 1o e. om
Theorem	2onn 6576	The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
|- 2o e. om
Theorem	3onn 6577	The ordinal 3 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 3o e. om
Theorem	4onn 6578	The ordinal 4 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 4o e. om
Theorem	2ssom 6579	The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.)
|- 2o C_ om
Theorem	nnm1 6580	Multiply an element of om by 1o. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( A .o 1o ) = A )
Theorem	nnm2 6581	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 6582	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 6583*	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 6584*	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 6585	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 6586	Extend the definition of a wff to include the equivalence predicate.
wff R Er A
Syntax	cec 6587	Extend the definition of a class to include equivalence class.
class [ A ] R
Syntax	cqs 6588	Extend the definition of a class to include quotient set.
class ( A /. R )
Definition	df-er 6589	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 6590 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 6609, ersymb 6603, and ertr 6604. (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 6590*	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 6591	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 6590). 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 6592. (Contributed by NM, 23-Jul-1995.)
|- [ A ] R = ( R " { A } )
Theorem	dfec2 6592*	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 6593	An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995.)
|- ( R e. B -> [ A ] R e. _V )
Theorem	ecexr 6594	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 6595*	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 6596	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 6597	Equality theorem for equivalence predicate. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( A = B -> ( R Er A <-> R Er B ) )
Theorem	errel 6598	An equivalence relation is a relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> Rel R )
Theorem	erdm 6599	The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> dom R = A )
Theorem	ercl 6600	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 )