P. 60 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 5901-6000   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-ref 5901*	Define the set of all reflexive relationships over a base set. (Contributed by SF, 19-Feb-2015.)
⊢ Ref = {⟨r, a⟩ ∣ ∀x ∈ a xrx}
Definition	df-antisym 5902*	Define the set of all antisymmetric relationships over a base set. (Contributed by SF, 19-Feb-2015.)
⊢ Antisym = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a ((xry ∧ yrx) → x = y)}
Definition	df-partial 5903	Define the set of all partial orderings over a base set. (Contributed by SF, 19-Feb-2015.)
⊢ Po = (( Ref ∩ Trans ) ∩ Antisym )
Definition	df-connex 5904*	Define the set of all connected relationships over a base set. (Contributed by SF, 19-Feb-2015.)
⊢ Connex = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (xry ∨ yrx)}
Definition	df-strict 5905	Define the set of all strict orderings over a base set. (Contributed by SF, 19-Feb-2015.)
⊢ Or = ( Po ∩ Connex )
Definition	df-found 5906*	Define the set of all founded relationships over a base set. (Contributed by SF, 19-Feb-2015.)
⊢ Fr = {⟨r, a⟩ ∣ ∀x((x ⊆ a ∧ x ≠ ∅) → ∃z ∈ x ∀y ∈ x (yrz → y = z))}
Definition	df-we 5907	Define the set of all well orderings over a base set. (Contributed by SF, 19-Feb-2015.)
⊢ We = ( Or ∩ Fr )
Definition	df-ext 5908*	Define the set of all extensional relationships over a base set. (Contributed by SF, 19-Feb-2015.)
⊢ Ext = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (∀z ∈ a (zrx ↔ zry) → x = y)}
Definition	df-sym 5909*	Define the set of all symmetric relationships over a base set. (Contributed by SF, 19-Feb-2015.)
⊢ Sym = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (xry → yrx)}
Definition	df-er 5910	Define the set of all equivalence relationships over a base set. (Contributed by SF, 19-Feb-2015.)
⊢ Er = ( Sym ∩ Trans )
Theorem	transex 5911	The class of all transitive relationships is a set. (Contributed by SF, 19-Feb-2015.)
⊢ Trans ∈ V
Theorem	refex 5912	The class of all reflexive relationships is a set. (Contributed by SF, 11-Mar-2015.)
⊢ Ref ∈ V
Theorem	antisymex 5913	The class of all antisymmetric relationships is a set. (Contributed by SF, 11-Mar-2015.)
⊢ Antisym ∈ V
Theorem	connexex 5914	The class of all connected relationships is a set. (Contributed by SF, 11-Mar-2015.)
⊢ Connex ∈ V
Theorem	foundex 5915	The class of all founded relationships is a set. (Contributed by SF, 19-Feb-2015.)
⊢ Fr ∈ V
Theorem	extex 5916	The class of all extensional relationships is a set. (Contributed by SF, 19-Feb-2015.)
⊢ Ext ∈ V
Theorem	symex 5917	The class of all symmetric relationships is a set. (Contributed by SF, 20-Feb-2015.)
⊢ Sym ∈ V
Theorem	partialex 5918	The class of all partial orderings is a set. (Contributed by SF, 11-Mar-2015.)
⊢ Po ∈ V
Theorem	strictex 5919	The class of all strict orderings is a set. (Contributed by SF, 19-Feb-2015.)
⊢ Or ∈ V
Theorem	weex 5920	The class of all well orderings is a set. (Contributed by SF, 19-Feb-2015.)
⊢ We ∈ V
Theorem	erex 5921	The class of all equivalence relationships is a set. (Contributed by SF, 20-Feb-2015.)
⊢ Er ∈ V
Theorem	trd 5922	Transitivity law in natural deduction form. (Contributed by SF, 20-Feb-2015.)
⊢ (φ → R Trans A)    &   ⊢ (φ → X ∈ A)    &   ⊢ (φ → Y ∈ A)    &   ⊢ (φ → Z ∈ A)    &   ⊢ (φ → XRY)    &   ⊢ (φ → YRZ)    ⇒   ⊢ (φ → XRZ)
Theorem	frd 5923*	Founded relationship in natural deduction form. (Contributed by SF, 12-Mar-2015.)
⊢ (φ → R Fr A)    &   ⊢ (φ → X ∈ V)    &   ⊢ (φ → X ⊆ A)    &   ⊢ (φ → X ≠ ∅)    ⇒   ⊢ (φ → ∃y ∈ X ∀z ∈ X (zRy → z = y))
Theorem	extd 5924*	Extensional relationship in natural deduction form. (Contributed by SF, 20-Feb-2015.)
⊢ (φ → R Ext A)    &   ⊢ (φ → X ∈ A)    &   ⊢ (φ → Y ∈ A)    &   ⊢ ((φ ∧ z ∈ A) → (zRX ↔ zRY))    ⇒   ⊢ (φ → X = Y)
Theorem	symd 5925	Symmetric relationship in natural deduction form. (Contributed by SF, 20-Feb-2015.)
⊢ (φ → R Sym A)    &   ⊢ (φ → X ∈ A)    &   ⊢ (φ → Y ∈ A)    &   ⊢ (φ → XRY)    ⇒   ⊢ (φ → YRX)
Theorem	trrd 5926*	Deduce transitivity from its properties. (Contributed by SF, 22-Feb-2015.)
⊢ (φ → R ∈ V)    &   ⊢ (φ → A ∈ W)    &   ⊢ ((φ ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A) ∧ (xRy ∧ yRz)) → xRz)    ⇒   ⊢ (φ → R Trans A)
Theorem	refrd 5927*	Deduce reflexivity from its properties. (Contributed by SF, 12-Mar-2015.)
⊢ (φ → R ∈ V)    &   ⊢ (φ → A ∈ W)    &   ⊢ ((φ ∧ x ∈ A) → xRx)    ⇒   ⊢ (φ → R Ref A)
Theorem	refd 5928	Natural deduction form of reflexivity. (Contributed by SF, 20-Mar-2015.)
⊢ (φ → R Ref A)    &   ⊢ (φ → X ∈ A)    ⇒   ⊢ (φ → XRX)
Theorem	antird 5929*	Deduce antisymmetry from its properties. (Contributed by SF, 12-Mar-2015.)
⊢ (φ → R ∈ V)    &   ⊢ (φ → A ∈ W)    &   ⊢ ((φ ∧ (x ∈ A ∧ y ∈ A) ∧ (xRy ∧ yRx)) → x = y)    ⇒   ⊢ (φ → R Antisym A)
Theorem	antid 5930	The antisymmetry property. (Contributed by SF, 18-Mar-2015.)
⊢ (φ → R Antisym A)    &   ⊢ (φ → X ∈ A)    &   ⊢ (φ → Y ∈ A)    &   ⊢ (φ → XRY)    &   ⊢ (φ → YRX)    ⇒   ⊢ (φ → X = Y)
Theorem	connexrd 5931*	Deduce connectivity from its properties. (Contributed by SF, 12-Mar-2015.)
⊢ (φ → R ∈ V)    &   ⊢ (φ → A ∈ W)    &   ⊢ ((φ ∧ x ∈ A ∧ y ∈ A) → (xRy ∨ yRx))    ⇒   ⊢ (φ → R Connex A)
Theorem	connexd 5932	The connectivity property. (Contributed by SF, 18-Mar-2015.)
⊢ (φ → R Connex A)    &   ⊢ (φ → X ∈ A)    &   ⊢ (φ → Y ∈ A)    ⇒   ⊢ (φ → (XRY ∨ YRX))
Theorem	ersymtr 5933	Equivalence relationship as symmetric, transitive relationship. (Contributed by SF, 22-Feb-2015.)
⊢ (R Er A ↔ (R Sym A ∧ R Trans A))
Theorem	porta 5934	Partial ordering as reflexive, transitive, antisymmetric relationship. (Contributed by SF, 12-Mar-2015.)
⊢ (R Po A ↔ (R Ref A ∧ R Trans A ∧ R Antisym A))
Theorem	sopc 5935	Linear ordering as partial, connected relationship. (Contributed by SF, 12-Mar-2015.)
⊢ (R Or A ↔ (R Po A ∧ R Connex A))
Theorem	frds 5936*	Substitution schema verson of frd 5923. (Contributed by SF, 19-Mar-2015.)
⊢ {x ∣ ψ} ∈ V    &   ⊢ (x = y → (ψ ↔ χ))    &   ⊢ (x = z → (ψ ↔ θ))    &   ⊢ (φ → R Fr A)    &   ⊢ (φ → ∃x ∈ A ψ)    ⇒   ⊢ (φ → ∃y ∈ A (χ ∧ ∀z ∈ A ((θ ∧ zRy) → z = y)))
Theorem	pod 5937*	A reflexive, transitive, and anti-symmetric ordering is a partial ordering. (Contributed by SF, 22-Feb-2015.)
⊢ (φ → R ∈ V)    &   ⊢ (φ → A ∈ W)    &   ⊢ ((φ ∧ x ∈ A) → xRx)    &   ⊢ ((φ ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A) ∧ (xRy ∧ yRz)) → xRz)    &   ⊢ ((φ ∧ (x ∈ A ∧ y ∈ A) ∧ (xRy ∧ yRx)) → x = y)    ⇒   ⊢ (φ → R Po A)
Theorem	sod 5938*	A reflexive, transitive, antisymmetric, and connected relationship is a strict ordering. (Contributed by SF, 12-Mar-2015.)
⊢ (φ → R ∈ V)    &   ⊢ (φ → A ∈ W)    &   ⊢ ((φ ∧ x ∈ A) → xRx)    &   ⊢ ((φ ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A) ∧ (xRy ∧ yRz)) → xRz)    &   ⊢ ((φ ∧ (x ∈ A ∧ y ∈ A) ∧ (xRy ∧ yRx)) → x = y)    &   ⊢ ((φ ∧ x ∈ A ∧ y ∈ A) → (xRy ∨ yRx))    ⇒   ⊢ (φ → R Or A)
Theorem	weds 5939*	Any property that holds for some element of a well-ordered set A has an R minimal element satisfying that property. (Contributed by SF, 20-Mar-2015.)
⊢ {x ∣ ψ} ∈ V    &   ⊢ (x = y → (ψ ↔ χ))    &   ⊢ (x = z → (ψ ↔ θ))    &   ⊢ (φ → R We A)    &   ⊢ (φ → ∃x ∈ A ψ)    ⇒   ⊢ (φ → ∃y ∈ A (χ ∧ ∀z ∈ A (θ → yRz)))
Theorem	po0 5940	Anything partially orders the empty set. (Contributed by SF, 12-Mar-2015.)
⊢ (φ → R ∈ V)    ⇒   ⊢ (φ → R Po ∅)
Theorem	connex0 5941	Anything is connected over the empty set. (Contributed by SF, 12-Mar-2015.)
⊢ (φ → R ∈ V)    ⇒   ⊢ (φ → R Connex ∅)
Theorem	so0 5942	Anything totally orders the empty set. (Contributed by SF, 12-Mar-2015.)
⊢ (φ → R ∈ V)    ⇒   ⊢ (φ → R Or ∅)
Theorem	iserd 5943*	A symmetric, transitive relationship is an equivalence relationship. (Contributed by SF, 22-Feb-2015.)
⊢ (φ → R ∈ V)    &   ⊢ (φ → A ∈ W)    &   ⊢ ((φ ∧ (x ∈ A ∧ y ∈ A) ∧ xRy) → yRx)    &   ⊢ ((φ ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A) ∧ (xRy ∧ yRz)) → xRz)    ⇒   ⊢ (φ → R Er A)
Theorem	ider 5944	The identity relationship is an equivalence relationship over the universe. (Contributed by SF, 22-Feb-2015.)
⊢ I Er V
Theorem	ssetpov 5945	The subset relationship partially orders the universe. (Contributed by SF, 12-Mar-2015.)
⊢ S Po V
2.4.2  Equivalence relations and classes
Syntax	cec 5946	Extend the definition of a class to include equivalence class.
class [A]R
Syntax	cqs 5947	Extend the definition of a class to include quotient set.
class (A / R)
Definition	df-ec 5948	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. 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 5949. (Contributed by set.mm contributors, 22-Feb-2015.)
⊢ [A]R = (R “ {A})
Theorem	dfec2 5949*	Alternate definition of R-coset of A. Definition 34 of [Suppes] p. 81. (Contributed by set.mm contributors, 22-Feb-2015.)
⊢ [A]R = {y ∣ ARy}
Theorem	ecexg 5950	An equivalence class modulo a set is a set. (Contributed by set.mm contributors, 24-Jul-1995.)
⊢ (R ∈ B → [A]R ∈ V)
Theorem	ecexr 5951	A nonempty equivalence class implies the representative is a set. (Contributed by set.mm contributors, 9-Jul-2014.)
⊢ (A ∈ [B]R → B ∈ V)
Definition	df-qs 5952*	Define quotient set. R is usually an equivalence relation. Definition of [Enderton] p. 58. (Contributed by set.mm contributors, 22-Feb-2015.)
⊢ (A / R) = {y ∣ ∃x ∈ A y = [x]R}
Theorem	ersym 5953	An equivalence relation is symmetric. (Contributed by set.mm contributors, 22-Feb-2015.)
⊢ (φ → R Er A)    &   ⊢ (φ → X ∈ A)    &   ⊢ (φ → Y ∈ A)    &   ⊢ (φ → XRY)    ⇒   ⊢ (φ → YRX)
Theorem	ersymb 5954	An equivalence relation is symmetric. (Contributed by set.mm contributors, 30-Jul-1995.) (Revised by set.mm contributors, 9-Jul-2014.)
⊢ (φ → R Er A)    &   ⊢ (φ → X ∈ A)    &   ⊢ (φ → Y ∈ A)    ⇒   ⊢ (φ → (XRY ↔ YRX))
Theorem	ertr 5955	An equivalence relation is transitive. (Contributed by set.mm contributors, 4-Jun-1995.) (Revised by set.mm contributors, 9-Jul-2014.)
⊢ (φ → R Er A)    &   ⊢ (φ → X ∈ A)    &   ⊢ (φ → Y ∈ A)    &   ⊢ (φ → Z ∈ A)    ⇒   ⊢ (φ → ((XRY ∧ YRZ) → XRZ))
Theorem	ertrd 5956	A transitivity relation for equivalences. (Contributed by set.mm contributors, 9-Jul-2014.)
⊢ (φ → R Er A)    &   ⊢ (φ → X ∈ A)    &   ⊢ (φ → Y ∈ A)    &   ⊢ (φ → Z ∈ A)    &   ⊢ (φ → XRY)    &   ⊢ (φ → YRZ)    ⇒   ⊢ (φ → XRZ)
Theorem	ertr2d 5957	A transitivity relation for equivalences. (Contributed by set.mm contributors, 9-Jul-2014.)
⊢ (φ → R Er A)    &   ⊢ (φ → X ∈ A)    &   ⊢ (φ → Y ∈ A)    &   ⊢ (φ → Z ∈ A)    &   ⊢ (φ → XRY)    &   ⊢ (φ → YRZ)    ⇒   ⊢ (φ → ZRX)
Theorem	ertr3d 5958	A transitivity relation for equivalences. (Contributed by set.mm contributors, 9-Jul-2014.)
⊢ (φ → R Er A)    &   ⊢ (φ → X ∈ A)    &   ⊢ (φ → Y ∈ A)    &   ⊢ (φ → Z ∈ A)    &   ⊢ (φ → YRX)    &   ⊢ (φ → YRZ)    ⇒   ⊢ (φ → XRZ)
Theorem	ertr4d 5959	A transitivity relation for equivalences. (Contributed by set.mm contributors, 9-Jul-2014.)
⊢ (φ → R Er A)    &   ⊢ (φ → X ∈ A)    &   ⊢ (φ → Y ∈ A)    &   ⊢ (φ → Z ∈ A)    &   ⊢ (φ → XRY)    &   ⊢ (φ → ZRY)    ⇒   ⊢ (φ → XRZ)
Theorem	erref 5960	An equivalence relation is reflexive on its field. Compare Theorem 3M of [Enderton] p. 56. (Contributed by set.mm contributors, 6-May-2013.)
⊢ (φ → R Er V)    &   ⊢ (φ → dom R = A)    &   ⊢ (φ → X ∈ A)    ⇒   ⊢ (φ → XRX)
Theorem	eqerlem 5961*	Lemma for eqer 5962. (Contributed by set.mm contributors, 17-Mar-2008.)
⊢ (x = y → A = B)    &   ⊢ R = {⟨x, y⟩ ∣ A = B}    ⇒   ⊢ (zRw ↔ [z / x]A = [w / x]A)
Theorem	eqer 5962*	Equivalence relation involving equality of dependent classes A(x) and B(y). (Contributed by set.mm contributors, 17-Mar-2008.)
⊢ (x = y → A = B)    &   ⊢ R = {⟨x, y⟩ ∣ A = B}    &   ⊢ R ∈ V    ⇒   ⊢ R Er V
Theorem	eceq1 5963	Equality theorem for equivalence class. (Contributed by set.mm contributors, 23-Jul-1995.)
⊢ (A = B → [A]C = [B]C)
Theorem	eceq2 5964	Equality theorem for equivalence class. (Contributed by set.mm contributors, 23-Jul-1995.)
⊢ (A = B → [C]A = [C]B)
Theorem	elec 5965	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by set.mm contributors, 9-Jul-2014.)
⊢ (A ∈ [B]R ↔ BRA)
Theorem	erdmrn 5966	The range and domain of an equivalence relation are equal. (Contributed by Rodolfo Medina, 11-Oct-2010.)
⊢ (R Er V → dom R = ran R)
Theorem	ecss 5967	An equivalence class is a subset of the domain. (Contributed by set.mm contributors, 6-Aug-1995.) (Revised by set.mm contributors, 9-Jul-2014.)
⊢ (φ → R Er V)    &   ⊢ (φ → dom R = X)    ⇒   ⊢ (φ → [A]R ⊆ X)
Theorem	ecdmn0 5968	A representative of a nonempty equivalence class belongs to the domain of the equivalence relation. (Contributed by set.mm contributors, 15-Feb-1996.) (Revised by set.mm contributors, 9-Jul-2014.)
⊢ (A ∈ dom R ↔ [A]R ≠ ∅)
Theorem	erth 5969	Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. (Contributed by set.mm contributors, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (φ → R Er V)    &   ⊢ (φ → dom R = X)    &   ⊢ (φ → A ∈ X)    &   ⊢ (φ → B ∈ V)    ⇒   ⊢ (φ → (ARB ↔ [A]R = [B]R))
Theorem	erth2 5970	Basic property of equivalence relations. Compare Theorem 73 of [Suppes] p. 82. Assumes membership of the second argument in the domain. (Contributed by set.mm contributors, 30-Jul-1995.) (Revised by set.mm contributors, 9-Jul-2014.)
⊢ (φ → R Er V)    &   ⊢ (φ → dom R = X)    &   ⊢ (φ → A ∈ V)    &   ⊢ (φ → B ∈ X)    ⇒   ⊢ (φ → (ARB ↔ [A]R = [B]R))
Theorem	erthi 5971	Basic property of equivalence relations. Part of Lemma 3N of [Enderton] p. 57. (Contributed by set.mm contributors, 30-Jul-1995.) (Revised by set.mm contributors, 9-Jul-2014.)
⊢ (φ → R Er V)    &   ⊢ (φ → ARB)    ⇒   ⊢ (φ → [A]R = [B]R)
Theorem	ereldm 5972	Equality of equivalence classes implies equivalence of domain membership. (Contributed by set.mm contributors, 28-Jan-1996.) (Revised by set.mm contributors, 9-Jul-2014.)
⊢ (φ → R Er V)    &   ⊢ (φ → dom R = X)    &   ⊢ (φ → [A]R = [B]R)    &   ⊢ (φ → A ∈ V)    &   ⊢ (φ → B ∈ W)    ⇒   ⊢ (φ → (A ∈ X ↔ B ∈ X))
Theorem	erdisj 5973	Equivalence classes do not overlap. In other words, two equivalence classes are either equal or disjoint. Theorem 74 of [Suppes] p. 83. (Contributed by set.mm contributors, 15-Jun-2004.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (R Er V → ([A]R = [B]R ∨ ([A]R ∩ [B]R) = ∅))
Theorem	ecidsn 5974	An equivalence class modulo the identity relation is a singleton. (Contributed by set.mm contributors, 24-Oct-2004.)
⊢ [A] I = {A}
Theorem	qseq1 5975	Equality theorem for quotient set. (Contributed by set.mm contributors, 23-Jul-1995.)
⊢ (A = B → (A / C) = (B / C))
Theorem	qseq2 5976	Equality theorem for quotient set. (Contributed by set.mm contributors, 23-Jul-1995.)
⊢ (A = B → (C / A) = (C / B))
Theorem	elqsg 5977*	Closed form of elqs 5978. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (B ∈ V → (B ∈ (A / R) ↔ ∃x ∈ A B = [x]R))
Theorem	elqs 5978*	Membership in a quotient set. (Contributed by set.mm contributors, 23-Jul-1995.) (Revised by set.mm contributors, 12-Nov-2008.)
⊢ B ∈ V    ⇒   ⊢ (B ∈ (A / R) ↔ ∃x ∈ A B = [x]R)
Theorem	elqsi 5979*	Membership in a quotient set. (Contributed by set.mm contributors, 23-Jul-1995.)
⊢ (B ∈ (A / R) → ∃x ∈ A B = [x]R)
Theorem	ecelqsg 5980	Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ ((R ∈ V ∧ B ∈ A) → [B]R ∈ (A / R))
Theorem	ecelqsi 5981	Membership of an equivalence class in a quotient set. (Contributed by set.mm contributors, 25-Jul-1995.) (Revised by set.mm contributors, 9-Jul-2014.)
⊢ R ∈ V    ⇒   ⊢ (B ∈ A → [B]R ∈ (A / R))
Theorem	ecopqsi 5982	"Closure" law for equivalence class of ordered pairs. (Contributed by set.mm contributors, 25-Mar-1996.)
⊢ R ∈ V    &   ⊢ S = ((A × A) / R)    ⇒   ⊢ ((B ∈ A ∧ C ∈ A) → [⟨B, C⟩]R ∈ S)
Theorem	qsexg 5983	A quotient set exists. (Contributed by FL, 19-May-2007.)
⊢ ((R ∈ V ∧ A ∈ W) → (A / R) ∈ V)
Theorem	qsex 5984	A quotient set exists. (Contributed by set.mm contributors, 14-Aug-1995.)
⊢ R ∈ V    &   ⊢ A ∈ V    ⇒   ⊢ (A / R) ∈ V
Theorem	uniqs 5985	The union of a quotient set. (Contributed by set.mm contributors, 9-Dec-2008.)
⊢ (R ∈ V → ∪(A / R) = (R “ A))
Theorem	uniqs2 5986	The union of a quotient set. (Contributed by set.mm contributors, 11-Jul-2014.)
⊢ (φ → R Er V)    &   ⊢ (φ → dom R = A)    &   ⊢ (φ → R ∈ V)    ⇒   ⊢ (φ → ∪(A / R) = A)
Theorem	qsss 5987	A quotient set is a set of subsets of the base set. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (φ → R Er V)    &   ⊢ (φ → dom R = A)    &   ⊢ (φ → R ∈ V)    ⇒   ⊢ (φ → (A / R) ⊆ ℘A)
Theorem	snec 5988	The singleton of an equivalence class. (Contributed by set.mm contributors, 29-Jan-1999.) (Revised by set.mm contributors, 9-Jul-2014.)
⊢ A ∈ V    ⇒   ⊢ {[A]R} = ({A} / R)
Theorem	ecqs 5989	Equivalence class in terms of quotient set. (Contributed by set.mm contributors, 29-Jan-1999.) (Revised by set.mm contributors, 15-Jan-2009.)
⊢ R ∈ V    ⇒   ⊢ [A]R = ∪({A} / R)
Theorem	ecid 5990	A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by set.mm contributors, 13-Aug-1995.) (Revised by set.mm contributors, 9-Jul-2014.)
⊢ A ∈ V    ⇒   ⊢ [A]◡ E = A
Theorem	qsid 5991	A set is equal to its quotient set mod converse epsilon. (Note: converse epsilon is not an equivalence relation.) (Contributed by set.mm contributors, 13-Aug-1995.) (Revised by set.mm contributors, 9-Jul-2014.)
⊢ (A / ◡ E ) = A
Theorem	ectocld 5992*	Implicit substitution of class for equivalence class. (Contributed by set.mm contributors, 9-Jul-2014.)
⊢ S = (B / R)    &   ⊢ ([x]R = A → (φ ↔ ψ))    &   ⊢ ((χ ∧ x ∈ B) → φ)    ⇒   ⊢ ((χ ∧ A ∈ S) → ψ)
Theorem	ectocl 5993*	Implicit substitution of class for equivalence class. (Contributed by set.mm contributors, 23-Jul-1995.) (Revised by set.mm contributors, 9-Jul-2014.)
⊢ S = (B / R)    &   ⊢ ([x]R = A → (φ ↔ ψ))    &   ⊢ (x ∈ B → φ)    ⇒   ⊢ (A ∈ S → ψ)
Theorem	elqsn0 5994	A quotient set doesn't contain the empty set. (Contributed by set.mm contributors, 24-Aug-1995.) (Revised by set.mm contributors, 21-Mar-2007.)
⊢ ((dom R = A ∧ B ∈ (A / R)) → B ≠ ∅)
Theorem	ecelqsdm 5995	Membership of an equivalence class in a quotient set. (Contributed by set.mm contributors, 30-Jul-1995.) (Revised by set.mm contributors, 21-Mar-2007.)
⊢ ((dom R = A ∧ [B]R ∈ (A / R)) → B ∈ A)
Theorem	qsdisj 5996	Members of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010.) (Revised by Mario Carneiro, 11-Jul-2014.)
⊢ (φ → R Er V)    &   ⊢ (φ → B ∈ (A / R))    &   ⊢ (φ → C ∈ (A / R))    ⇒   ⊢ (φ → (B = C ∨ (B ∩ C) = ∅))
Theorem	ecoptocl 5997*	Implicit substitution of class for equivalence class of ordered pair. (Contributed by set.mm contributors, 23-Jul-1995.)
⊢ S = ((B × C) / R)    &   ⊢ ([⟨x, y⟩]R = A → (φ ↔ ψ))    &   ⊢ ((x ∈ B ∧ y ∈ C) → φ)    ⇒   ⊢ (A ∈ S → ψ)
Theorem	2ecoptocl 5998*	Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by set.mm contributors, 23-Jul-1995.)
⊢ S = ((C × D) / R)    &   ⊢ ([⟨x, y⟩]R = A → (φ ↔ ψ))    &   ⊢ ([⟨z, w⟩]R = B → (ψ ↔ χ))    &   ⊢ (((x ∈ C ∧ y ∈ D) ∧ (z ∈ C ∧ w ∈ D)) → φ)    ⇒   ⊢ ((A ∈ S ∧ B ∈ S) → χ)
Theorem	3ecoptocl 5999*	Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by set.mm contributors, 9-Aug-1995.)
⊢ S = ((D × D) / R)    &   ⊢ ([⟨x, y⟩]R = A → (φ ↔ ψ))    &   ⊢ ([⟨z, w⟩]R = B → (ψ ↔ χ))    &   ⊢ ([⟨v, u⟩]R = C → (χ ↔ θ))    &   ⊢ (((x ∈ D ∧ y ∈ D) ∧ (z ∈ D ∧ w ∈ D) ∧ (v ∈ D ∧ u ∈ D)) → φ)    ⇒   ⊢ ((A ∈ S ∧ B ∈ S ∧ C ∈ S) → θ)
2.4.3  The mapping operation
Syntax	cmap 6000	Extend the definition of a class to include the mapping operation. (Read for A ↑m B, "the set of all functions that map from B to A.)
class ↑m