P. 68 of Theorem List - Intuitionistic Logic Explorer

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

Type	Label	Description
Statement
Theorem	onasuc 6701	Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵))
Theorem	oa1suc 6702	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.)
⊢ (𝐴 ∈ On → (𝐴 +o 1o) = suc 𝐴)
Theorem	o1p1e2 6703	1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.)
⊢ (1o +o 1o) = 2o
Theorem	oawordi 6704	Weak ordering property of ordinal addition. (Contributed by Jim Kingdon, 27-Jul-2019.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐶 +o 𝐴) ⊆ (𝐶 +o 𝐵)))
Theorem	oawordriexmid 6705*	A weak ordering property of ordinal addition which implies excluded middle. The property is proposition 8.7 of [TakeutiZaring] p. 59. Compare with oawordi 6704. (Contributed by Jim Kingdon, 15-May-2022.)
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) → (𝑎 ⊆ 𝑏 → (𝑎 +o 𝑐) ⊆ (𝑏 +o 𝑐)))    ⇒   ⊢ (𝜑 ∨ ¬ 𝜑)
Theorem	oaword1 6706	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.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ⊆ (𝐴 +o 𝐵))
Theorem	omsuc 6707	Multiplication with successor. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) +o 𝐴))
Theorem	onmsuc 6708	Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) +o 𝐴))
2.6.25  Natural number arithmetic
Theorem	nna0 6709	Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.)
⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴)
Theorem	nnm0 6710	Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.)
⊢ (𝐴 ∈ ω → (𝐴 ·o ∅) = ∅)
Theorem	nnasuc 6711	Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵))
Theorem	nnmsuc 6712	Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) +o 𝐴))
Theorem	nna0r 6713	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.)
⊢ (𝐴 ∈ ω → (∅ +o 𝐴) = 𝐴)
Theorem	nnm0r 6714	Multiplication with zero. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ (𝐴 ∈ ω → (∅ ·o 𝐴) = ∅)
Theorem	nnacl 6715	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.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +o 𝐵) ∈ ω)
Theorem	nnmcl 6716	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.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·o 𝐵) ∈ ω)
Theorem	nnacli 6717	ω is closed under addition. Inference form of nnacl 6715. (Contributed by Scott Fenton, 20-Apr-2012.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 ∈ ω    ⇒   ⊢ (𝐴 +o 𝐵) ∈ ω
Theorem	nnmcli 6718	ω is closed under multiplication. Inference form of nnmcl 6716. (Contributed by Scott Fenton, 20-Apr-2012.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 ∈ ω    ⇒   ⊢ (𝐴 ·o 𝐵) ∈ ω
Theorem	nnacom 6719	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.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +o 𝐵) = (𝐵 +o 𝐴))
Theorem	nnaass 6720	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.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +o 𝐵) +o 𝐶) = (𝐴 +o (𝐵 +o 𝐶)))
Theorem	nndi 6721	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.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ·o (𝐵 +o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶)))
Theorem	nnmass 6722	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.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ·o 𝐵) ·o 𝐶) = (𝐴 ·o (𝐵 ·o 𝐶)))
Theorem	nnmsucr 6723	Multiplication with successor. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ·o 𝐵) = ((𝐴 ·o 𝐵) +o 𝐵))
Theorem	nnmcom 6724	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.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·o 𝐵) = (𝐵 ·o 𝐴))
Theorem	nndir 6725	Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +o 𝐵) ·o 𝐶) = ((𝐴 ·o 𝐶) +o (𝐵 ·o 𝐶)))
Theorem	nnsucelsuc 6726	Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucelsucr 4632, but the forward direction, for all ordinals, implies excluded middle as seen as onsucelsucexmid 4654. (Contributed by Jim Kingdon, 25-Aug-2019.)
⊢ (𝐵 ∈ ω → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵))
Theorem	nnsucsssuc 6727	Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4633, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4651. (Contributed by Jim Kingdon, 25-Aug-2019.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵))
Theorem	nntri3or 6728	Trichotomy for natural numbers. (Contributed by Jim Kingdon, 25-Aug-2019.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
Theorem	nntri2 6729	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)))
Theorem	nnsucuniel 6730	Given an element 𝐴 of the union of a natural number 𝐵, suc 𝐴 is an element of 𝐵 itself. The reverse direction holds for all ordinals (sucunielr 4634). The forward direction for all ordinals implies excluded middle (ordsucunielexmid 4655). (Contributed by Jim Kingdon, 13-Mar-2022.)
⊢ (𝐵 ∈ ω → (𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵))
Theorem	nntri1 6731	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))
Theorem	nntri3 6732	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-May-2020.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 = 𝐵 ↔ (¬ 𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴)))
Theorem	nntri2or2 6733	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-Sep-2021.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))
Theorem	nndceq 6734	Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p. (varies). For the specific case where 𝐵 is zero, see nndceq0 4742. (Contributed by Jim Kingdon, 31-Aug-2019.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → DECID 𝐴 = 𝐵)
Theorem	nndcel 6735	Set membership between two natural numbers is decidable. (Contributed by Jim Kingdon, 6-Sep-2019.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → DECID 𝐴 ∈ 𝐵)
Theorem	nnsseleq 6736	For natural numbers, inclusion is equivalent to membership or equality. (Contributed by Jim Kingdon, 16-Sep-2021.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	nnsssuc 6737	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.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵))
Theorem	nntr2 6738	Transitive law for natural numbers. (Contributed by Jim Kingdon, 22-Jul-2023.)
⊢ ((𝐴 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	dcdifsnid 6739*	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 3842 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 17-Jun-2022.)
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
Theorem	fnsnsplitdc 6740*	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.)
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐹 = ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {⟨𝑋, (𝐹‘𝑋)⟩}))
Theorem	funresdfunsndc 6741*	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.)
⊢ ((∀𝑥 ∈ dom 𝐹∀𝑦 ∈ dom 𝐹DECID 𝑥 = 𝑦 ∧ Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹) → ((𝐹 ↾ (V ∖ {𝑋})) ∪ {⟨𝑋, (𝐹‘𝑋)⟩}) = 𝐹)
Theorem	nndifsnid 6742	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 3842 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 31-Aug-2021.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
Theorem	nnaordi 6743	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.)
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵)))
Theorem	nnaord 6744	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.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 ↔ (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵)))
Theorem	nnaordr 6745	Ordering property of addition of natural numbers. (Contributed by NM, 9-Nov-2002.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 ↔ (𝐴 +o 𝐶) ∈ (𝐵 +o 𝐶)))
Theorem	nnaword 6746	Weak ordering property of addition. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝐶 +o 𝐴) ⊆ (𝐶 +o 𝐵)))
Theorem	nnacan 6747	Cancellation law for addition of natural numbers. (Contributed by NM, 27-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +o 𝐵) = (𝐴 +o 𝐶) ↔ 𝐵 = 𝐶))
Theorem	nnaword1 6748	Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐴 ⊆ (𝐴 +o 𝐵))
Theorem	nnaword2 6749	Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐴 ⊆ (𝐵 +o 𝐴))
Theorem	nnawordi 6750	Adding to both sides of an inequality in ω. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 12-May-2012.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +o 𝐶) ⊆ (𝐵 +o 𝐶)))
Theorem	nnmordi 6751	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.)
⊢ (((𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅ ∈ 𝐶) → (𝐴 ∈ 𝐵 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵)))
Theorem	nnmord 6752	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.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶) ↔ (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵)))
Theorem	nnmword 6753	Weak ordering property of ordinal multiplication. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅ ∈ 𝐶) → (𝐴 ⊆ 𝐵 ↔ (𝐶 ·o 𝐴) ⊆ (𝐶 ·o 𝐵)))
Theorem	nnmcan 6754	Cancellation law for multiplication of natural numbers. (Contributed by NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅ ∈ 𝐴) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ 𝐵 = 𝐶))
Theorem	1onn 6755	One is a natural number. (Contributed by NM, 29-Oct-1995.)
⊢ 1o ∈ ω
Theorem	2onn 6756	The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
⊢ 2o ∈ ω
Theorem	3onn 6757	The ordinal 3 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 3o ∈ ω
Theorem	4onn 6758	The ordinal 4 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 4o ∈ ω
Theorem	2ssom 6759	The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.)
⊢ 2o ⊆ ω
Theorem	nnm1 6760	Multiply an element of ω by 1o. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ω → (𝐴 ·o 1o) = 𝐴)
Theorem	nnm2 6761	Multiply an element of ω by 2o. (Contributed by Scott Fenton, 18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ω → (𝐴 ·o 2o) = (𝐴 +o 𝐴))
Theorem	nn2m 6762	Multiply an element of ω by 2o. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ω → (2o ·o 𝐴) = (𝐴 +o 𝐴))
Theorem	nnaordex 6763*	Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88. (Contributed by NM, 5-Dec-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))
Theorem	nnawordex 6764*	Equivalence for weak ordering of natural numbers. (Contributed by NM, 8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵))
Theorem	nnm00 6765	The product of two natural numbers is zero iff at least one of them is zero. (Contributed by Jim Kingdon, 11-Nov-2004.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·o 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅)))
2.6.26  Equivalence relations and classes
Syntax	wer 6766	Extend the definition of a wff to include the equivalence predicate.
wff 𝑅 Er 𝐴
Syntax	cec 6767	Extend the definition of a class to include equivalence class.
class [𝐴]𝑅
Syntax	cqs 6768	Extend the definition of a class to include quotient set.
class (𝐴 / 𝑅)
Definition	df-er 6769	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 6770 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 6789, ersymb 6783, and ertr 6784. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 2-Nov-2015.)
⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
Theorem	dfer2 6770*	Alternate definition of equivalence predicate. (Contributed by NM, 3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
Definition	df-ec 6771	Define the 𝑅-coset of 𝐴. Exercise 35 of [Enderton] p. 61. This is called the equivalence class of 𝐴 modulo 𝑅 when 𝑅 is an equivalence relation (i.e. when Er 𝑅; see dfer2 6770). In this case, 𝐴 is a representative (member) of the equivalence class [𝐴]𝑅, which contains all sets that are equivalent to 𝐴. Definition of [Enderton] p. 57 uses the notation [𝐴] (subscript) 𝑅, although we simply follow the brackets by 𝑅 since we don't have subscripted expressions. For an alternate definition, see dfec2 6772. (Contributed by NM, 23-Jul-1995.)
⊢ [𝐴]𝑅 = (𝑅 “ {𝐴})
Theorem	dfec2 6772*	Alternate definition of 𝑅-coset of 𝐴. Definition 34 of [Suppes] p. 81. (Contributed by NM, 3-Jan-1997.) (Proof shortened by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → [𝐴]𝑅 = {𝑦 ∣ 𝐴𝑅𝑦})
Theorem	ecexg 6773	An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995.)
⊢ (𝑅 ∈ 𝐵 → [𝐴]𝑅 ∈ V)
Theorem	ecexr 6774	An inhabited equivalence class implies the representative is a set. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ [𝐵]𝑅 → 𝐵 ∈ V)
Definition	df-qs 6775*	Define quotient set. 𝑅 is usually an equivalence relation. Definition of [Enderton] p. 58. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
Theorem	ereq1 6776	Equality theorem for equivalence predicate. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 = 𝑆 → (𝑅 Er 𝐴 ↔ 𝑆 Er 𝐴))
Theorem	ereq2 6777	Equality theorem for equivalence predicate. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝐴 = 𝐵 → (𝑅 Er 𝐴 ↔ 𝑅 Er 𝐵))
Theorem	errel 6778	An equivalence relation is a relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → Rel 𝑅)
Theorem	erdm 6779	The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → dom 𝑅 = 𝐴)
Theorem	ercl 6780	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑋)
Theorem	ersym 6781	An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐵𝑅𝐴)
Theorem	ercl2 6782	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑋)
Theorem	ersymb 6783	An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴))
Theorem	ertr 6784	An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    ⇒   ⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))
Theorem	ertrd 6785	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	ertr2d 6786	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐴)
Theorem	ertr3d 6787	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐵𝑅𝐴)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	ertr4d 6788	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	erref 6789	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.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐴)
Theorem	ercnv 6790	The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → ◡𝑅 = 𝑅)
Theorem	errn 6791	The range and domain of an equivalence relation are equal. (Contributed by Rodolfo Medina, 11-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → ran 𝑅 = 𝐴)
Theorem	erssxp 6792	An equivalence relation is a subset of the cartesian product of the field. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → 𝑅 ⊆ (𝐴 × 𝐴))
Theorem	erex 6793	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.)
⊢ (𝑅 Er 𝐴 → (𝐴 ∈ 𝑉 → 𝑅 ∈ V))
Theorem	erexb 6794	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.)
⊢ (𝑅 Er 𝐴 → (𝑅 ∈ V ↔ 𝐴 ∈ V))
Theorem	iserd 6795*	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.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦𝑅𝑥)    &   ⊢ ((𝜑 ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥))    ⇒   ⊢ (𝜑 → 𝑅 Er 𝐴)
Theorem	brdifun 6796	Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)))
Theorem	swoer 6797*	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.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    ⇒   ⊢ (𝜑 → 𝑅 Er 𝑋)
Theorem	swoord1 6798*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶))
Theorem	swoord2 6799*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵))
Theorem	eqerlem 6800*	Lemma for eqer 6801. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵}    ⇒   ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴)