P. 77 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7601-7700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnmcan 7601	Cancellation law for multiplication of natural numbers. (Contributed by NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅ ∈ 𝐴) → ((𝐴 ·𝑜 𝐵) = (𝐴 ·𝑜 𝐶) ↔ 𝐵 = 𝐶))
Theorem	nnmwordi 7602	Weak ordering property of multiplication. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐶 ·𝑜 𝐴) ⊆ (𝐶 ·𝑜 𝐵)))
Theorem	nnmwordri 7603	Weak ordering property of ordinal multiplication. Proposition 8.21 of [TakeutiZaring] p. 63, limited to natural numbers. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 ·𝑜 𝐶) ⊆ (𝐵 ·𝑜 𝐶)))
Theorem	nnawordex 7604*	Equivalence for weak ordering of natural numbers. (Contributed by NM, 8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝐵))
Theorem	nnaordex 7605*	Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88. (Contributed by NM, 5-Dec-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
Theorem	1onn 7606	One is a natural number. (Contributed by NM, 29-Oct-1995.)
⊢ 1𝑜 ∈ ω
Theorem	2onn 7607	The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
⊢ 2𝑜 ∈ ω
Theorem	3onn 7608	The ordinal 3 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 3𝑜 ∈ ω
Theorem	4onn 7609	The ordinal 4 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 4𝑜 ∈ ω
Theorem	oaabslem 7610	Lemma for oaabs 7611. (Contributed by NM, 9-Dec-2004.)
⊢ ((ω ∈ On ∧ 𝐴 ∈ ω) → (𝐴 +𝑜 ω) = ω)
Theorem	oaabs 7611	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.)
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω ⊆ 𝐵) → (𝐴 +𝑜 𝐵) = 𝐵)
Theorem	oaabs2 7612	The absorption law oaabs 7611 is also a property of higher powers of ω. (Contributed by Mario Carneiro, 29-May-2015.)
⊢ (((𝐴 ∈ (ω ↑𝑜 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑𝑜 𝐶) ⊆ 𝐵) → (𝐴 +𝑜 𝐵) = 𝐵)
Theorem	omabslem 7613	Lemma for omabs 7614. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ ((ω ∈ On ∧ 𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → (𝐴 ·𝑜 ω) = ω)
Theorem	omabs 7614	Ordinal multiplication is also absorbed by powers of ω. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) → (𝐴 ·𝑜 (ω ↑𝑜 𝐵)) = (ω ↑𝑜 𝐵))
Theorem	nnm1 7615	Multiply an element of ω by 1𝑜. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ω → (𝐴 ·𝑜 1𝑜) = 𝐴)
Theorem	nnm2 7616	Multiply an element of ω by 2𝑜. (Contributed by Scott Fenton, 18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ω → (𝐴 ·𝑜 2𝑜) = (𝐴 +𝑜 𝐴))
Theorem	nn2m 7617	Multiply an element of ω by 2𝑜. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ω → (2𝑜 ·𝑜 𝐴) = (𝐴 +𝑜 𝐴))
Theorem	nnneo 7618	If a natural number is even, its successor is odd. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 = (2𝑜 ·𝑜 𝐴)) → ¬ suc 𝐶 = (2𝑜 ·𝑜 𝐵))
Theorem	nneob 7619*	A natural number is even iff its successor is odd. (Contributed by NM, 26-Jan-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ (𝐴 ∈ ω → (∃𝑥 ∈ ω 𝐴 = (2𝑜 ·𝑜 𝑥) ↔ ¬ ∃𝑥 ∈ ω suc 𝐴 = (2𝑜 ·𝑜 𝑥)))
Theorem	omsmolem 7620*	Lemma for omsmo 7621. (Contributed by NM, 30-Nov-2003.) (Revised by David Abernethy, 1-Jan-2014.)
⊢ (𝑦 ∈ ω → (((𝐴 ⊆ On ∧ 𝐹:ω⟶𝐴) ∧ ∀𝑥 ∈ ω (𝐹‘𝑥) ∈ (𝐹‘suc 𝑥)) → (𝑧 ∈ 𝑦 → (𝐹‘𝑧) ∈ (𝐹‘𝑦))))
Theorem	omsmo 7621*	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.)
⊢ (((𝐴 ⊆ On ∧ 𝐹:ω⟶𝐴) ∧ ∀𝑥 ∈ ω (𝐹‘𝑥) ∈ (𝐹‘suc 𝑥)) → 𝐹:ω–1-1→𝐴)
Theorem	omopthlem1 7622	Lemma for omopthi 7624. (Contributed by Scott Fenton, 18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐶 ∈ ω    ⇒   ⊢ (𝐴 ∈ 𝐶 → ((𝐴 ·𝑜 𝐴) +𝑜 (𝐴 ·𝑜 2𝑜)) ∈ (𝐶 ·𝑜 𝐶))
Theorem	omopthlem2 7623	Lemma for omopthi 7624. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 ∈ ω    &   ⊢ 𝐶 ∈ ω    &   ⊢ 𝐷 ∈ ω    ⇒   ⊢ ((𝐴 +𝑜 𝐵) ∈ 𝐶 → ¬ ((𝐶 ·𝑜 𝐶) +𝑜 𝐷) = (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵))
Theorem	omopthi 7624	An ordered pair theorem for ω. Theorem 17.3 of [Quine] p. 124. This proof is adapted from nn0opthi 12919. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 ∈ ω    &   ⊢ 𝐶 ∈ ω    &   ⊢ 𝐷 ∈ ω    ⇒   ⊢ ((((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	omopth 7625	An ordered pair theorem for finite integers. Analogous to nn0opthi 12919. (Contributed by Scott Fenton, 1-May-2012.)
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐶 ∈ ω ∧ 𝐷 ∈ ω)) → ((((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
2.4.20  Equivalence relations and classes
Syntax	wer 7626	Extend the definition of a wff to include the equivalence predicate.
wff 𝑅 Er 𝐴
Syntax	cec 7627	Extend the definition of a class to include equivalence class.
class [𝐴]𝑅
Syntax	cqs 7628	Extend the definition of a class to include quotient set.
class (𝐴 / 𝑅)
Definition	df-er 7629	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 7630 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 7649, ersymb 7643, and ertr 7644. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 2-Nov-2015.)
⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
Theorem	dfer2 7630*	Alternate definition of equivalence predicate. (Contributed by NM, 3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
Definition	df-ec 7631	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 7630). 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 7632. (Contributed by NM, 23-Jul-1995.)
⊢ [𝐴]𝑅 = (𝑅 “ {𝐴})
Theorem	dfec2 7632*	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 7633	An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995.)
⊢ (𝑅 ∈ 𝐵 → [𝐴]𝑅 ∈ V)
Theorem	ecexr 7634	A nonempty equivalence class implies the representative is a set. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ [𝐵]𝑅 → 𝐵 ∈ V)
Definition	df-qs 7635*	Define quotient set. 𝑅 is usually an equivalence relation. Definition of [Enderton] p. 58. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
Theorem	ereq1 7636	Equality theorem for equivalence predicate. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 = 𝑆 → (𝑅 Er 𝐴 ↔ 𝑆 Er 𝐴))
Theorem	ereq2 7637	Equality theorem for equivalence predicate. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝐴 = 𝐵 → (𝑅 Er 𝐴 ↔ 𝑅 Er 𝐵))
Theorem	errel 7638	An equivalence relation is a relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → Rel 𝑅)
Theorem	erdm 7639	The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → dom 𝑅 = 𝐴)
Theorem	ercl 7640	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑋)
Theorem	ersym 7641	An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐵𝑅𝐴)
Theorem	ercl2 7642	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑋)
Theorem	ersymb 7643	An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴))
Theorem	ertr 7644	An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    ⇒   ⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))
Theorem	ertrd 7645	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	ertr2d 7646	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐴)
Theorem	ertr3d 7647	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐵𝑅𝐴)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	ertr4d 7648	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	erref 7649	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 7650	The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → ◡𝑅 = 𝑅)
Theorem	errn 7651	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 7652	An equivalence relation is a subset of the cartesian product of the field. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → 𝑅 ⊆ (𝐴 × 𝐴))
Theorem	erex 7653	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 7654	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 7655*	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 7656*	A reflexive, symmetric, transitive relation is an equivalence relation on its domain. Inference version of iserd 7655, 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 7657*	Alternate proof of iseri 7656, avoiding the usage of trud 1484 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	brdifun 7658	Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)))
Theorem	swoer 7659*	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 7660*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶))
Theorem	swoord2 7661*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵))
Theorem	swoso 7662*	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 7663*	Lemma for eqer 7664. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵}    ⇒   ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴)
Theorem	eqer 7664*	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	eqerOLD 7665*	Obsolete proof of eqer 7664 as of 1-May-2021. Equivalence relation involving equality of dependent classes 𝐴(𝑥) and 𝐵(𝑦). (Contributed by NM, 17-Mar-2008.) (Revised by Mario Carneiro, 12-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵}    ⇒   ⊢ 𝑅 Er V
Theorem	ider 7666	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 7667	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 7668	Obsolete proof of 0er 7667 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 7669	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
Theorem	eceq1d 7670	Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)
Theorem	eceq2 7671	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → [𝐶]𝐴 = [𝐶]𝐵)
Theorem	elecg 7672	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴))
Theorem	elec 7673	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)
Theorem	relelec 7674	Membership in an equivalence class when 𝑅 is a relation. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴))
Theorem	ecss 7675	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 7676	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 7677	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 7678	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 7679	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 7680	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 7681	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 7682	An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.)
⊢ [𝐴] I = {𝐴}
Theorem	qseq1 7683	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → (𝐴 / 𝐶) = (𝐵 / 𝐶))
Theorem	qseq2 7684	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → (𝐶 / 𝐴) = (𝐶 / 𝐵))
Theorem	elqsg 7685*	Closed form of elqs 7686. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅))
Theorem	elqs 7686*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)
Theorem	elqsi 7687*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐵 ∈ (𝐴 / 𝑅) → ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)
Theorem	elqsecl 7688*	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 7689	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 7690	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 7691	"Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996.)
⊢ 𝑅 ∈ V    &   ⊢ 𝑆 = ((𝐴 × 𝐴) / 𝑅)    ⇒   ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → [⟨𝐵, 𝐶⟩]𝑅 ∈ 𝑆)
Theorem	qsexg 7692	A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 / 𝑅) ∈ V)
Theorem	qsex 7693	A quotient set exists. (Contributed by NM, 14-Aug-1995.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 / 𝑅) ∈ V
Theorem	uniqs 7694	The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
⊢ (𝑅 ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴))
Theorem	qsss 7695	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 7696	The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∪ (𝐴 / 𝑅) = 𝐴)
Theorem	snec 7697	The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {[𝐴]𝑅} = ({𝐴} / 𝑅)
Theorem	ecqs 7698	Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.)
⊢ 𝑅 ∈ V    ⇒   ⊢ [𝐴]𝑅 = ∪ ({𝐴} / 𝑅)
Theorem	ecid 7699	A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ [𝐴]◡ E = 𝐴
Theorem	qsid 7700	A set is equal to its quotient set mod converse epsilon. (Note: converse epsilon is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 / ◡ E ) = 𝐴