P. 88 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8701-8800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	naddword1 8701	Weak-ordering principle for natural addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ⊆ (𝐴 +no 𝐵))
Theorem	naddword2 8702	Weak-ordering principle for natural addition. (Contributed by Scott Fenton, 15-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ⊆ (𝐵 +no 𝐴))
Theorem	naddunif 8703*	Uniformity theorem for natural addition. If 𝐴 is the upper bound of 𝑋 and 𝐵 is the upper bound of 𝑌, then (𝐴 +no 𝐵) can be expressed in terms of 𝑋 and 𝑌. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐴 = ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥})    &   ⊢ (𝜑 → 𝐵 = ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦})    ⇒   ⊢ (𝜑 → (𝐴 +no 𝐵) = ∩ {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧})
Theorem	naddasslem1 8704*	Lemma for naddass 8706. Expand out the expression for natural addition of three arguments. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +no 𝐵) +no 𝐶) = ∩ {𝑥 ∈ On ∣ (∀𝑎 ∈ 𝐴 ((𝑎 +no 𝐵) +no 𝐶) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝐵 ((𝐴 +no 𝑏) +no 𝐶) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝐶 ((𝐴 +no 𝐵) +no 𝑐) ∈ 𝑥)})
Theorem	naddasslem2 8705*	Lemma for naddass 8706. Expand out the expression for natural addition of three arguments. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 +no (𝐵 +no 𝐶)) = ∩ {𝑥 ∈ On ∣ (∀𝑎 ∈ 𝐴 (𝑎 +no (𝐵 +no 𝐶)) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝐵 (𝐴 +no (𝑏 +no 𝐶)) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝐶 (𝐴 +no (𝐵 +no 𝑐)) ∈ 𝑥)})
Theorem	naddass 8706	Natural ordinal addition is associative. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +no 𝐵) +no 𝐶) = (𝐴 +no (𝐵 +no 𝐶)))
Theorem	nadd32 8707	Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +no 𝐵) +no 𝐶) = ((𝐴 +no 𝐶) +no 𝐵))
Theorem	nadd4 8708	Rearragement of terms in a quadruple sum. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ((𝐴 +no 𝐵) +no (𝐶 +no 𝐷)) = ((𝐴 +no 𝐶) +no (𝐵 +no 𝐷)))
Theorem	nadd42 8709	Rearragement of terms in a quadruple sum. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ((𝐴 +no 𝐵) +no (𝐶 +no 𝐷)) = ((𝐴 +no 𝐶) +no (𝐷 +no 𝐵)))
Theorem	naddel12 8710	Natural addition to both sides of ordinal less-than. (Contributed by Scott Fenton, 7-Feb-2025.)
⊢ ((𝐶 ∈ On ∧ 𝐷 ∈ On) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 +no 𝐵) ∈ (𝐶 +no 𝐷)))
Theorem	naddsuc2 8711	Natural addition with successor. (Contributed by RP, 1-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no suc 𝐵) = suc (𝐴 +no 𝐵))
Theorem	naddoa 8712	Natural addition of a natural is the same as regular addition. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +no 𝐵) = (𝐴 +o 𝐵))
Theorem	omnaddcl 8713	The naturals are closed under natural addition. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +no 𝐵) ∈ ω)
2.4.26  Equivalence relations and classes
Syntax	wer 8714	Extend the definition of a wff to include the equivalence predicate.
wff 𝑅 Er 𝐴
Syntax	cec 8715	Extend the definition of a class to include equivalence class.
class [𝐴]𝑅
Syntax	cqs 8716	Extend the definition of a class to include quotient set.
class (𝐴 / 𝑅)
Definition	df-er 8717	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 8718 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 8737, ersymb 8731, and ertr 8732. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 2-Nov-2015.)
⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
Theorem	dfer2 8718*	Alternate definition of equivalence predicate. (Contributed by NM, 3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
Definition	df-ec 8719	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 8718). 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 8720. (Contributed by NM, 23-Jul-1995.)
⊢ [𝐴]𝑅 = (𝑅 “ {𝐴})
Theorem	dfec2 8720*	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 8721	An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995.)
⊢ (𝑅 ∈ 𝐵 → [𝐴]𝑅 ∈ V)
Theorem	ecexr 8722	A nonempty equivalence class implies the representative is a set. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ [𝐵]𝑅 → 𝐵 ∈ V)
Definition	df-qs 8723*	Define quotient set. 𝑅 is usually an equivalence relation. Definition of [Enderton] p. 58. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
Theorem	ereq1 8724	Equality theorem for equivalence predicate. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 = 𝑆 → (𝑅 Er 𝐴 ↔ 𝑆 Er 𝐴))
Theorem	ereq2 8725	Equality theorem for equivalence predicate. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝐴 = 𝐵 → (𝑅 Er 𝐴 ↔ 𝑅 Er 𝐵))
Theorem	errel 8726	An equivalence relation is a relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → Rel 𝑅)
Theorem	erdm 8727	The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → dom 𝑅 = 𝐴)
Theorem	ercl 8728	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑋)
Theorem	ersym 8729	An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐵𝑅𝐴)
Theorem	ercl2 8730	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑋)
Theorem	ersymb 8731	An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴))
Theorem	ertr 8732	An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    ⇒   ⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))
Theorem	ertrd 8733	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	ertr2d 8734	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐴)
Theorem	ertr3d 8735	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐵𝑅𝐴)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	ertr4d 8736	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	erref 8737	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 8738	The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → ◡𝑅 = 𝑅)
Theorem	errn 8739	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 8740	An equivalence relation is a subset of the cartesian product of the field. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → 𝑅 ⊆ (𝐴 × 𝐴))
Theorem	erex 8741	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 8742	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 8743*	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	iseri 8744*	A reflexive, symmetric, transitive relation is an equivalence relation on its domain. Inference version of iserd 8743, which avoids the need to provide a "dummy antecedent" 𝜑 if there is no natural one to choose. (Contributed by AV, 30-Apr-2021.)
⊢ Rel 𝑅    &   ⊢ (𝑥𝑅𝑦 → 𝑦𝑅𝑥)    &   ⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)    &   ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥)    ⇒   ⊢ 𝑅 Er 𝐴
Theorem	iseriALT 8745*	Alternate proof of iseri 8744, avoiding the usage of mptru 1547 and ⊤ 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 𝑅    &   ⊢ (𝑥𝑅𝑦 → 𝑦𝑅𝑥)    &   ⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)    &   ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥)    ⇒   ⊢ 𝑅 Er 𝐴
Theorem	brinxper 8746*	Conditions for a reflexive, symmetric and transitive binary relation to be an equivalence relation over a class 𝑉. (Contributed by AV, 11-Jun-2025.)
⊢ (𝑥 ∈ 𝑉 → 𝑥 ∼ 𝑥)    &   ⊢ (𝑥 ∈ 𝑉 → (𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥))    &   ⊢ (𝑥 ∈ 𝑉 → ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧))    ⇒   ⊢ ( ∼ ∩ (𝑉 × 𝑉)) Er 𝑉
Theorem	brdifun 8747	Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)))
Theorem	swoer 8748*	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 8749*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶))
Theorem	swoord2 8750*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵))
Theorem	swoso 8751*	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.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ∧ 𝑥𝑅𝑦)) → 𝑥 = 𝑦)    ⇒   ⊢ (𝜑 → < Or 𝑌)
Theorem	eqerlem 8752*	Lemma for eqer 8753. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵}    ⇒   ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴)
Theorem	eqer 8753*	Equivalence relation involving equality of dependent classes 𝐴(𝑥) and 𝐵(𝑦). (Contributed by NM, 17-Mar-2008.) (Revised by Mario Carneiro, 12-Aug-2015.) (Proof shortened by AV, 1-May-2021.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵}    ⇒   ⊢ 𝑅 Er V
Theorem	ider 8754	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 8755	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	eceq1 8756	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
Theorem	eceq1d 8757	Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)
Theorem	eceq2 8758	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → [𝐶]𝐴 = [𝐶]𝐵)
Theorem	eceq2i 8759	Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, inference version. (Contributed by Peter Mazsa, 11-May-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ [𝐶]𝐴 = [𝐶]𝐵
Theorem	eceq2d 8760	Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → [𝐶]𝐴 = [𝐶]𝐵)
Theorem	elecg 8761	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴))
Theorem	ecref 8762	All elements are in their own equivalence class. (Contributed by Thierry Arnoux, 14-Feb-2025.)
⊢ ((𝑅 Er 𝑋 ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ [𝐴]𝑅)
Theorem	elec 8763	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)
Theorem	relelec 8764	Membership in an equivalence class when 𝑅 is a relation. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴))
Theorem	ecss 8765	An equivalence class is a subset of the domain. (Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    ⇒   ⊢ (𝜑 → [𝐴]𝑅 ⊆ 𝑋)
Theorem	ecdmn0 8766	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.)
⊢ (𝐴 ∈ dom 𝑅 ↔ [𝐴]𝑅 ≠ ∅)
Theorem	ereldm 8767	Equality of equivalence classes implies equivalence of domain membership. (Contributed by NM, 28-Jan-1996.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅)    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋))
Theorem	erth 8768	Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))
Theorem	erth2 8769	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.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))
Theorem	erthi 8770	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.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅)
Theorem	erdisj 8771	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.)
⊢ (𝑅 Er 𝑋 → ([𝐴]𝑅 = [𝐵]𝑅 ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅))
Theorem	ecidsn 8772	An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.)
⊢ [𝐴] I = {𝐴}
Theorem	qseq1 8773	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → (𝐴 / 𝐶) = (𝐵 / 𝐶))
Theorem	qseq2 8774	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → (𝐶 / 𝐴) = (𝐶 / 𝐵))
Theorem	qseq2i 8775	Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 / 𝐴) = (𝐶 / 𝐵)
Theorem	qseq1d 8776	Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐶))
Theorem	qseq2d 8777	Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 / 𝐴) = (𝐶 / 𝐵))
Theorem	qseq12 8778	Equality theorem for quotient set. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 / 𝐶) = (𝐵 / 𝐷))
Theorem	0qs 8779	Quotient set with the empty set. (Contributed by Peter Mazsa, 14-Sep-2019.)
⊢ (∅ / 𝑅) = ∅
Theorem	elqsg 8780*	Closed form of elqs 8781. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅))
Theorem	elqs 8781*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)
Theorem	elqsi 8782*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐵 ∈ (𝐴 / 𝑅) → ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)
Theorem	elqsecl 8783*	Membership in a quotient set by an equivalence class according to ∼. (Contributed by Alexander van der Vekens, 12-Apr-2018.) (Revised by AV, 30-Apr-2021.)
⊢ (𝐵 ∈ 𝑋 → (𝐵 ∈ (𝑊 / ∼ ) ↔ ∃𝑥 ∈ 𝑊 𝐵 = {𝑦 ∣ 𝑥 ∼ 𝑦}))
Theorem	ecelqsg 8784	Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 ∈ (𝐴 / 𝑅))
Theorem	ecelqsi 8785	Membership of an equivalence class in a quotient set. (Contributed by NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑅 ∈ V    ⇒   ⊢ (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ (𝐴 / 𝑅))
Theorem	ecopqsi 8786	"Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996.)
⊢ 𝑅 ∈ V    &   ⊢ 𝑆 = ((𝐴 × 𝐴) / 𝑅)    ⇒   ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → [⟨𝐵, 𝐶⟩]𝑅 ∈ 𝑆)
Theorem	qsexg 8787	A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 / 𝑅) ∈ V)
Theorem	qsex 8788	A quotient set exists. (Contributed by NM, 14-Aug-1995.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 / 𝑅) ∈ V
Theorem	uniqs 8789	The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
⊢ (𝑅 ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴))
Theorem	qsss 8790	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.)
⊢ (𝜑 → 𝑅 Er 𝐴)    ⇒   ⊢ (𝜑 → (𝐴 / 𝑅) ⊆ 𝒫 𝐴)
Theorem	uniqs2 8791	The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∪ (𝐴 / 𝑅) = 𝐴)
Theorem	snec 8792	The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {[𝐴]𝑅} = ({𝐴} / 𝑅)
Theorem	ecqs 8793	Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.)
⊢ 𝑅 ∈ V    ⇒   ⊢ [𝐴]𝑅 = ∪ ({𝐴} / 𝑅)
Theorem	ecid 8794	A set is equal to its coset under the converse membership relation. (Note: the converse membership relation is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ [𝐴]◡ E = 𝐴
Theorem	qsid 8795	A set is equal to its quotient set modulo the converse membership relation. (Note: the converse membership relation is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 / ◡ E ) = 𝐴
Theorem	ectocld 8796*	Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑆 = (𝐵 / 𝑅)    &   ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → 𝜑)    ⇒   ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓)
Theorem	ectocl 8797*	Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑆 = (𝐵 / 𝑅)    &   ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ 𝐵 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑆 → 𝜓)
Theorem	elqsn0 8798	A quotient set does not contain the empty set. (Contributed by NM, 24-Aug-1995.)
⊢ ((dom 𝑅 = 𝐴 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → 𝐵 ≠ ∅)
Theorem	ecelqsdm 8799	Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995.)
⊢ ((dom 𝑅 = 𝐴 ∧ [𝐵]𝑅 ∈ (𝐴 / 𝑅)) → 𝐵 ∈ 𝐴)
Theorem	xpider 8800	A Cartesian square is an equivalence relation (in general, it is not a poset). (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝐴 × 𝐴) Er 𝐴