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-antisym 5901*	Define the set of all antisymmetric relationships over a base set. (Contributed by SF, 19-Feb-2015.)
|- Antisym = {<.r, a>. | A.x e. a A.y e. a ((xry /\ yrx) -> x = y)}
Definition	df-partial 5902	Define the set of all partial orderings over a base set. (Contributed by SF, 19-Feb-2015.)
|- Po = (( Ref i^i Trans ) i^i Antisym )
Definition	df-connex 5903*	Define the set of all connected relationships over a base set. (Contributed by SF, 19-Feb-2015.)
|- Connex = {<.r, a>. | A.x e. a A.y e. a (xry \/ yrx)}
Definition	df-strict 5904	Define the set of all strict orderings over a base set. (Contributed by SF, 19-Feb-2015.)
|- Or = ( Po i^i Connex )
Definition	df-found 5905*	Define the set of all founded relationships over a base set. (Contributed by SF, 19-Feb-2015.)
|- Fr = {<.r, a>. | A.x((x C_ a /\ x =/= (/)) -> E.z e. x A.y e. x (yrz -> y = z))}
Definition	df-we 5906	Define the set of all well orderings over a base set. (Contributed by SF, 19-Feb-2015.)
|- We = ( Or i^i Fr )
Definition	df-ext 5907*	Define the set of all extensional relationships over a base set. (Contributed by SF, 19-Feb-2015.)
|- Ext = {<.r, a>. | A.x e. a A.y e. a (A.z e. a (zrx <-> zry) -> x = y)}
Definition	df-sym 5908*	Define the set of all symmetric relationships over a base set. (Contributed by SF, 19-Feb-2015.)
|- Sym = {<.r, a>. | A.x e. a A.y e. a (xry -> yrx)}
Definition	df-er 5909	Define the set of all equivalence relationships over a base set. (Contributed by SF, 19-Feb-2015.)
|- Er = ( Sym i^i Trans )
Theorem	transex 5910	The class of all transitive relationships is a set. (Contributed by SF, 19-Feb-2015.)
|- Trans e. _V
Theorem	refex 5911	The class of all reflexive relationships is a set. (Contributed by SF, 11-Mar-2015.)
|- Ref e. _V
Theorem	antisymex 5912	The class of all antisymmetric relationships is a set. (Contributed by SF, 11-Mar-2015.)
|- Antisym e. _V
Theorem	connexex 5913	The class of all connected relationships is a set. (Contributed by SF, 11-Mar-2015.)
|- Connex e. _V
Theorem	foundex 5914	The class of all founded relationships is a set. (Contributed by SF, 19-Feb-2015.)
|- Fr e. _V
Theorem	extex 5915	The class of all extensional relationships is a set. (Contributed by SF, 19-Feb-2015.)
|- Ext e. _V
Theorem	symex 5916	The class of all symmetric relationships is a set. (Contributed by SF, 20-Feb-2015.)
|- Sym e. _V
Theorem	partialex 5917	The class of all partial orderings is a set. (Contributed by SF, 11-Mar-2015.)
|- Po e. _V
Theorem	strictex 5918	The class of all strict orderings is a set. (Contributed by SF, 19-Feb-2015.)
|- Or e. _V
Theorem	weex 5919	The class of all well orderings is a set. (Contributed by SF, 19-Feb-2015.)
|- We e. _V
Theorem	erex 5920	The class of all equivalence relationships is a set. (Contributed by SF, 20-Feb-2015.)
|- Er e. _V
Theorem	trd 5921	Transitivity law in natural deduction form. (Contributed by SF, 20-Feb-2015.)
|- (ph -> R Trans A)   &   |- (ph -> X e. A)   &   |- (ph -> Y e. A)   &   |- (ph -> Z e. A)   &   |- (ph -> XRY)   &   |- (ph -> YRZ)   =>   |- (ph -> XRZ)
Theorem	frd 5922*	Founded relationship in natural deduction form. (Contributed by SF, 12-Mar-2015.)
|- (ph -> R Fr A)   &   |- (ph -> X e. V)   &   |- (ph -> X C_ A)   &   |- (ph -> X =/= (/))   =>   |- (ph -> E.y e. X A.z e. X (zRy -> z = y))
Theorem	extd 5923*	Extensional relationship in natural deduction form. (Contributed by SF, 20-Feb-2015.)
|- (ph -> R Ext A)   &   |- (ph -> X e. A)   &   |- (ph -> Y e. A)   &   |- ((ph /\ z e. A) -> (zRX <-> zRY))   =>   |- (ph -> X = Y)
Theorem	symd 5924	Symmetric relationship in natural deduction form. (Contributed by SF, 20-Feb-2015.)
|- (ph -> R Sym A)   &   |- (ph -> X e. A)   &   |- (ph -> Y e. A)   &   |- (ph -> XRY)   =>   |- (ph -> YRX)
Theorem	trrd 5925*	Deduce transitivity from its properties. (Contributed by SF, 22-Feb-2015.)
|- (ph -> R e. V)   &   |- (ph -> A e. W)   &   |- ((ph /\ (x e. A /\ y e. A /\ z e. A) /\ (xRy /\ yRz)) -> xRz)   =>   |- (ph -> R Trans A)
Theorem	refrd 5926*	Deduce reflexitiviy from its properties. (Contributed by SF, 12-Mar-2015.)
|- (ph -> R e. V)   &   |- (ph -> A e. W)   &   |- ((ph /\ x e. A) -> xRx)   =>   |- (ph -> R Ref A)
Theorem	refd 5927	Natural deduction form of reflexitivity. (Contributed by SF, 20-Mar-2015.)
|- (ph -> R Ref A)   &   |- (ph -> X e. A)   =>   |- (ph -> XRX)
Theorem	antird 5928*	Deduce antisymmetry from its properties. (Contributed by SF, 12-Mar-2015.)
|- (ph -> R e. V)   &   |- (ph -> A e. W)   &   |- ((ph /\ (x e. A /\ y e. A) /\ (xRy /\ yRx)) -> x = y)   =>   |- (ph -> R Antisym A)
Theorem	antid 5929	The antisymmetry property. (Contributed by SF, 18-Mar-2015.)
|- (ph -> R Antisym A)   &   |- (ph -> X e. A)   &   |- (ph -> Y e. A)   &   |- (ph -> XRY)   &   |- (ph -> YRX)   =>   |- (ph -> X = Y)
Theorem	connexrd 5930*	Deduce connectivity from its properties. (Contributed by SF, 12-Mar-2015.)
|- (ph -> R e. V)   &   |- (ph -> A e. W)   &   |- ((ph /\ x e. A /\ y e. A) -> (xRy \/ yRx))   =>   |- (ph -> R Connex A)
Theorem	connexd 5931	The connectivity property. (Contributed by SF, 18-Mar-2015.)
|- (ph -> R Connex A)   &   |- (ph -> X e. A)   &   |- (ph -> Y e. A)   =>   |- (ph -> (XRY \/ YRX))
Theorem	ersymtr 5932	Equivalence relationship as symmetric, transitive relationship. (Contributed by SF, 22-Feb-2015.)
|- (R Er A <-> (R Sym A /\ R Trans A))
Theorem	porta 5933	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 5934	Linear ordering as partial, connected relationship. (Contributed by SF, 12-Mar-2015.)
|- (R Or A <-> (R Po A /\ R Connex A))
Theorem	frds 5935*	Substitution schema verson of frd 5922. (Contributed by SF, 19-Mar-2015.)
|- {x | ps} e. _V   &   |- (x = y -> (ps <-> ch))   &   |- (x = z -> (ps <-> th))   &   |- (ph -> R Fr A)   &   |- (ph -> E.x e. A ps)   =>   |- (ph -> E.y e. A (ch /\ A.z e. A ((th /\ zRy) -> z = y)))
Theorem	pod 5936*	A reflexive, transitive, and anti-symmetric ordering is a partial ordering. (Contributed by SF, 22-Feb-2015.)
|- (ph -> R e. V)   &   |- (ph -> A e. W)   &   |- ((ph /\ x e. A) -> xRx)   &   |- ((ph /\ (x e. A /\ y e. A /\ z e. A) /\ (xRy /\ yRz)) -> xRz)   &   |- ((ph /\ (x e. A /\ y e. A) /\ (xRy /\ yRx)) -> x = y)   =>   |- (ph -> R Po A)
Theorem	sod 5937*	A reflexive, transitive, antisymmetric, and connected relationship is a strict ordering. (Contributed by SF, 12-Mar-2015.)
|- (ph -> R e. V)   &   |- (ph -> A e. W)   &   |- ((ph /\ x e. A) -> xRx)   &   |- ((ph /\ (x e. A /\ y e. A /\ z e. A) /\ (xRy /\ yRz)) -> xRz)   &   |- ((ph /\ (x e. A /\ y e. A) /\ (xRy /\ yRx)) -> x = y)   &   |- ((ph /\ x e. A /\ y e. A) -> (xRy \/ yRx))   =>   |- (ph -> R Or A)
Theorem	weds 5938*	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 | ps} e. _V   &   |- (x = y -> (ps <-> ch))   &   |- (x = z -> (ps <-> th))   &   |- (ph -> R We A)   &   |- (ph -> E.x e. A ps)   =>   |- (ph -> E.y e. A (ch /\ A.z e. A (th -> yRz)))
Theorem	po0 5939	Anything partially orders the empty set. (Contributed by SF, 12-Mar-2015.)
|- (ph -> R e. V)   =>   |- (ph -> R Po (/))
Theorem	connex0 5940	Anything is connected over the empty set. (Contributed by SF, 12-Mar-2015.)
|- (ph -> R e. V)   =>   |- (ph -> R Connex (/))
Theorem	so0 5941	Anything totally orders the empty set. (Contributed by SF, 12-Mar-2015.)
|- (ph -> R e. V)   =>   |- (ph -> R Or (/))
Theorem	iserd 5942*	A symmetric, transitive relationship is an equivalence relationship. (Contributed by SF, 22-Feb-2015.)
|- (ph -> R e. V)   &   |- (ph -> A e. W)   &   |- ((ph /\ (x e. A /\ y e. A) /\ xRy) -> yRx)   &   |- ((ph /\ (x e. A /\ y e. A /\ z e. A) /\ (xRy /\ yRz)) -> xRz)   =>   |- (ph -> R Er A)
Theorem	ider 5943	The identity relationship is an equivalence relationship over the universe. (Contributed by SF, 22-Feb-2015.)
|- _I Er _V
Theorem	ssetpov 5944	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 5945	Extend the definition of a class to include equivalence class.
class [A]R
Syntax	cqs 5946	Extend the definition of a class to include quotient set.
class (A/.R)
Definition	df-ec 5947	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 5948. (Contributed by set.mm contributors, 22-Feb-2015.)
|- [A]R = (R"{A})
Theorem	dfec2 5948*	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 5949	An equivalence class modulo a set is a set. (Contributed by set.mm contributors, 24-Jul-1995.)
|- (R e. B -> [A]R e. _V)
Theorem	ecexr 5950	A nonempty equivalence class implies the representative is a set. (Contributed by set.mm contributors, 9-Jul-2014.)
|- (A e. [B]R -> B e. _V)
Definition	df-qs 5951*	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 | E.x e. A y = [x]R}
Theorem	ersym 5952	An equivalence relation is symmetric. (Contributed by set.mm contributors, 22-Feb-2015.)
|- (ph -> R Er A)   &   |- (ph -> X e. A)   &   |- (ph -> Y e. A)   &   |- (ph -> XRY)   =>   |- (ph -> YRX)
Theorem	ersymb 5953	An equivalence relation is symmetric. (Contributed by set.mm contributors, 30-Jul-1995.) (Revised by set.mm contributors, 9-Jul-2014.)
|- (ph -> R Er A)   &   |- (ph -> X e. A)   &   |- (ph -> Y e. A)   =>   |- (ph -> (XRY <-> YRX))
Theorem	ertr 5954	An equivalence relation is transitive. (Contributed by set.mm contributors, 4-Jun-1995.) (Revised by set.mm contributors, 9-Jul-2014.)
|- (ph -> R Er A)   &   |- (ph -> X e. A)   &   |- (ph -> Y e. A)   &   |- (ph -> Z e. A)   =>   |- (ph -> ((XRY /\ YRZ) -> XRZ))
Theorem	ertrd 5955	A transitivity relation for equivalences. (Contributed by set.mm contributors, 9-Jul-2014.)
|- (ph -> R Er A)   &   |- (ph -> X e. A)   &   |- (ph -> Y e. A)   &   |- (ph -> Z e. A)   &   |- (ph -> XRY)   &   |- (ph -> YRZ)   =>   |- (ph -> XRZ)
Theorem	ertr2d 5956	A transitivity relation for equivalences. (Contributed by set.mm contributors, 9-Jul-2014.)
|- (ph -> R Er A)   &   |- (ph -> X e. A)   &   |- (ph -> Y e. A)   &   |- (ph -> Z e. A)   &   |- (ph -> XRY)   &   |- (ph -> YRZ)   =>   |- (ph -> ZRX)
Theorem	ertr3d 5957	A transitivity relation for equivalences. (Contributed by set.mm contributors, 9-Jul-2014.)
|- (ph -> R Er A)   &   |- (ph -> X e. A)   &   |- (ph -> Y e. A)   &   |- (ph -> Z e. A)   &   |- (ph -> YRX)   &   |- (ph -> YRZ)   =>   |- (ph -> XRZ)
Theorem	ertr4d 5958	A transitivity relation for equivalences. (Contributed by set.mm contributors, 9-Jul-2014.)
|- (ph -> R Er A)   &   |- (ph -> X e. A)   &   |- (ph -> Y e. A)   &   |- (ph -> Z e. A)   &   |- (ph -> XRY)   &   |- (ph -> ZRY)   =>   |- (ph -> XRZ)
Theorem	erref 5959	An equivalence relation is reflexive on its field. Compare Theorem 3M of [Enderton] p. 56. (Contributed by set.mm contributors, 6-May-2013.)
|- (ph -> R Er _V)   &   |- (ph -> dom R = A)   &   |- (ph -> X e. A)   =>   |- (ph -> XRX)
Theorem	eqerlem 5960*	Lemma for eqer 5961. (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 5961*	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 e. _V   =>   |- R Er _V
Theorem	eceq1 5962	Equality theorem for equivalence class. (Contributed by set.mm contributors, 23-Jul-1995.)
|- (A = B -> [A]C = [B]C)
Theorem	eceq2 5963	Equality theorem for equivalence class. (Contributed by set.mm contributors, 23-Jul-1995.)
|- (A = B -> [C]A = [C]B)
Theorem	elec 5964	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by set.mm contributors, 9-Jul-2014.)
|- (A e. [B]R <-> BRA)
Theorem	erdmrn 5965	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 5966	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.)
|- (ph -> R Er _V)   &   |- (ph -> dom R = X)   =>   |- (ph -> [A]R C_ X)
Theorem	ecdmn0 5967	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 e. dom R <-> [A]R =/= (/))
Theorem	erth 5968	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.)
|- (ph -> R Er _V)   &   |- (ph -> dom R = X)   &   |- (ph -> A e. X)   &   |- (ph -> B e. V)   =>   |- (ph -> (ARB <-> [A]R = [B]R))
Theorem	erth2 5969	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.)
|- (ph -> R Er _V)   &   |- (ph -> dom R = X)   &   |- (ph -> A e. V)   &   |- (ph -> B e. X)   =>   |- (ph -> (ARB <-> [A]R = [B]R))
Theorem	erthi 5970	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.)
|- (ph -> R Er _V)   &   |- (ph -> ARB)   =>   |- (ph -> [A]R = [B]R)
Theorem	ereldm 5971	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.)
|- (ph -> R Er _V)   &   |- (ph -> dom R = X)   &   |- (ph -> [A]R = [B]R)   &   |- (ph -> A e. V)   &   |- (ph -> B e. W)   =>   |- (ph -> (A e. X <-> B e. X))
Theorem	erdisj 5972	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 i^i [B]R) = (/)))
Theorem	ecidsn 5973	An equivalence class modulo the identity relation is a singleton. (Contributed by set.mm contributors, 24-Oct-2004.)
|- [A] _I = {A}
Theorem	qseq1 5974	Equality theorem for quotient set. (Contributed by set.mm contributors, 23-Jul-1995.)
|- (A = B -> (A/.C) = (B/.C))
Theorem	qseq2 5975	Equality theorem for quotient set. (Contributed by set.mm contributors, 23-Jul-1995.)
|- (A = B -> (C/.A) = (C/.B))
Theorem	elqsg 5976*	Closed form of elqs 5977. (Contributed by Rodolfo Medina, 12-Oct-2010.)
|- (B e. V -> (B e. (A/.R) <-> E.x e. A B = [x]R))
Theorem	elqs 5977*	Membership in a quotient set. (Contributed by set.mm contributors, 23-Jul-1995.) (Revised by set.mm contributors, 12-Nov-2008.)
|- B e. _V   =>   |- (B e. (A/.R) <-> E.x e. A B = [x]R)
Theorem	elqsi 5978*	Membership in a quotient set. (Contributed by set.mm contributors, 23-Jul-1995.)
|- (B e. (A/.R) -> E.x e. A B = [x]R)
Theorem	ecelqsg 5979	Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ((R e. V /\ B e. A) -> [B]R e. (A/.R))
Theorem	ecelqsi 5980	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 e. _V   =>   |- (B e. A -> [B]R e. (A/.R))
Theorem	ecopqsi 5981	"Closure" law for equivalence class of ordered pairs. (Contributed by set.mm contributors, 25-Mar-1996.)
|- R e. _V   &   |- S = ((A X. A)/.R)   =>   |- ((B e. A /\ C e. A) -> [<.B, C>.]R e. S)
Theorem	qsexg 5982	A quotient set exists. (Contributed by FL, 19-May-2007.)
|- ((R e. V /\ A e. W) -> (A/.R) e. _V)
Theorem	qsex 5983	A quotient set exists. (Contributed by set.mm contributors, 14-Aug-1995.)
|- R e. _V   &   |- A e. _V   =>   |- (A/.R) e. _V
Theorem	uniqs 5984	The union of a quotient set. (Contributed by set.mm contributors, 9-Dec-2008.)
|- (R e. V -> U.(A/.R) = (R"A))
Theorem	uniqs2 5985	The union of a quotient set. (Contributed by set.mm contributors, 11-Jul-2014.)
|- (ph -> R Er _V)   &   |- (ph -> dom R = A)   &   |- (ph -> R e. V)   =>   |- (ph -> U.(A/.R) = A)
Theorem	qsss 5986	A quotient set is a set of subsets of the base set. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- (ph -> R Er _V)   &   |- (ph -> dom R = A)   &   |- (ph -> R e. V)   =>   |- (ph -> (A/.R) C_ ~PA)
Theorem	snec 5987	The singleton of an equivalence class. (Contributed by set.mm contributors, 29-Jan-1999.) (Revised by set.mm contributors, 9-Jul-2014.)
|- A e. _V   =>   |- {[A]R} = ({A}/.R)
Theorem	ecqs 5988	Equivalence class in terms of quotient set. (Contributed by set.mm contributors, 29-Jan-1999.) (Revised by set.mm contributors, 15-Jan-2009.)
|- R e. _V   =>   |- [A]R = U.({A}/.R)
Theorem	ecid 5989	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 e. _V   =>   |- [A]`' _E = A
Theorem	qsid 5990	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 5991*	Implicit substitution of class for equivalence class. (Contributed by set.mm contributors, 9-Jul-2014.)
|- S = (B/.R)   &   |- ([x]R = A -> (ph <-> ps))   &   |- ((ch /\ x e. B) -> ph)   =>   |- ((ch /\ A e. S) -> ps)
Theorem	ectocl 5992*	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 -> (ph <-> ps))   &   |- (x e. B -> ph)   =>   |- (A e. S -> ps)
Theorem	elqsn0 5993	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 e. (A/.R)) -> B =/= (/))
Theorem	ecelqsdm 5994	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 e. (A/.R)) -> B e. A)
Theorem	qsdisj 5995	Members of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010.) (Revised by Mario Carneiro, 11-Jul-2014.)
|- (ph -> R Er _V)   &   |- (ph -> B e. (A/.R))   &   |- (ph -> C e. (A/.R))   =>   |- (ph -> (B = C \/ (B i^i C) = (/)))
Theorem	ecoptocl 5996*	Implicit substitution of class for equivalence class of ordered pair. (Contributed by set.mm contributors, 23-Jul-1995.)
|- S = ((B X. C)/.R)   &   |- ([<.x, y>.]R = A -> (ph <-> ps))   &   |- ((x e. B /\ y e. C) -> ph)   =>   |- (A e. S -> ps)
Theorem	2ecoptocl 5997*	Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by set.mm contributors, 23-Jul-1995.)
|- S = ((C X. D)/.R)   &   |- ([<.x, y>.]R = A -> (ph <-> ps))   &   |- ([<.z, w>.]R = B -> (ps <-> ch))   &   |- (((x e. C /\ y e. D) /\ (z e. C /\ w e. D)) -> ph)   =>   |- ((A e. S /\ B e. S) -> ch)
Theorem	3ecoptocl 5998*	Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by set.mm contributors, 9-Aug-1995.)
|- S = ((D X. D)/.R)   &   |- ([<.x, y>.]R = A -> (ph <-> ps))   &   |- ([<.z, w>.]R = B -> (ps <-> ch))   &   |- ([<.v, u>.]R = C -> (ch <-> th))   &   |- (((x e. D /\ y e. D) /\ (z e. D /\ w e. D) /\ (v e. D /\ u e. D)) -> ph)   =>   |- ((A e. S /\ B e. S /\ C e. S) -> th)
2.4.3  The mapping operation
Syntax	cmap 5999	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
Syntax	cpm 6000	Extend the definition of a class to include the partial mapping operation. (Read for A ^m B, "the set of all partial functions that map from B to A.)
class ^pm