P. 64 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6301-6400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nndcel 6301	Set membership between two natural numbers is decidable. (Contributed by Jim Kingdon, 6-Sep-2019.)
|- ( ( A e. om /\ B e. om ) -> DECID A e. B )
Theorem	nnsseleq 6302	For natural numbers, inclusion is equivalent to membership or equality. (Contributed by Jim Kingdon, 16-Sep-2021.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> ( A e. B \/ A = B ) ) )
Theorem	dcdifsnid 6303*	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 3605 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 17-Jun-2022.)
|- ( ( A. x e. A A. y e. A DECID x = y /\ B e. A ) -> ( ( A \ { B } ) u. { B } ) = A )
Theorem	fnsnsplitdc 6304*	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.)
|- ( ( A. x e. A A. y e. A DECID x = y /\ F Fn A /\ X e. A ) -> F = ( ( F |` ( A \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )
Theorem	funresdfunsndc 6305*	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.)
|- ( ( A. x e. dom F A. y e. dom FDECID x = y /\ Fun F /\ X e. dom F ) -> ( ( F |` ( _V \ { X } ) ) u. { <. X , ( F ` X ) >. } ) = F )
Theorem	nndifsnid 6306	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 3605 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 31-Aug-2021.)
|- ( ( A e. om /\ B e. A ) -> ( ( A \ { B } ) u. { B } ) = A )
Theorem	nnaordi 6307	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.)
|- ( ( B e. om /\ C e. om ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
Theorem	nnaord 6308	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.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A e. B <-> ( C +o A ) e. ( C +o B ) ) )
Theorem	nnaordr 6309	Ordering property of addition of natural numbers. (Contributed by NM, 9-Nov-2002.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A e. B <-> ( A +o C ) e. ( B +o C ) ) )
Theorem	nnaword 6310	Weak ordering property of addition. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B <-> ( C +o A ) C_ ( C +o B ) ) )
Theorem	nnacan 6311	Cancellation law for addition of natural numbers. (Contributed by NM, 27-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A +o B ) = ( A +o C ) <-> B = C ) )
Theorem	nnaword1 6312	Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> A C_ ( A +o B ) )
Theorem	nnaword2 6313	Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
|- ( ( A e. om /\ B e. om ) -> A C_ ( B +o A ) )
Theorem	nnawordi 6314	Adding to both sides of an inequality in om (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 12-May-2012.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B -> ( A +o C ) C_ ( B +o C ) ) )
Theorem	nnmordi 6315	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.)
|- ( ( ( B e. om /\ C e. om ) /\ (/) e. C ) -> ( A e. B -> ( C .o A ) e. ( C .o B ) ) )
Theorem	nnmord 6316	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.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A e. B /\ (/) e. C ) <-> ( C .o A ) e. ( C .o B ) ) )
Theorem	nnmword 6317	Weak ordering property of ordinal multiplication. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( ( ( A e. om /\ B e. om /\ C e. om ) /\ (/) e. C ) -> ( A C_ B <-> ( C .o A ) C_ ( C .o B ) ) )
Theorem	nnmcan 6318	Cancellation law for multiplication of natural numbers. (Contributed by NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( ( A e. om /\ B e. om /\ C e. om ) /\ (/) e. A ) -> ( ( A .o B ) = ( A .o C ) <-> B = C ) )
Theorem	1onn 6319	One is a natural number. (Contributed by NM, 29-Oct-1995.)
|- 1o e. om
Theorem	2onn 6320	The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
|- 2o e. om
Theorem	3onn 6321	The ordinal 3 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 3o e. om
Theorem	4onn 6322	The ordinal 4 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 4o e. om
Theorem	nnm1 6323	Multiply an element of om by 1o. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( A .o 1o ) = A )
Theorem	nnm2 6324	Multiply an element of om by 2o (Contributed by Scott Fenton, 18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( A .o 2o ) = ( A +o A ) )
Theorem	nn2m 6325	Multiply an element of om by 2o (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( 2o .o A ) = ( A +o A ) )
Theorem	nnaordex 6326*	Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88. (Contributed by NM, 5-Dec-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A e. B <-> E. x e. om ( (/) e. x /\ ( A +o x ) = B ) ) )
Theorem	nnawordex 6327*	Equivalence for weak ordering of natural numbers. (Contributed by NM, 8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> E. x e. om ( A +o x ) = B ) )
Theorem	nnm00 6328	The product of two natural numbers is zero iff at least one of them is zero. (Contributed by Jim Kingdon, 11-Nov-2004.)
|- ( ( A e. om /\ B e. om ) -> ( ( A .o B ) = (/) <-> ( A = (/) \/ B = (/) ) ) )
2.6.24  Equivalence relations and classes
Syntax	wer 6329	Extend the definition of a wff to include the equivalence predicate.
wff R Er A
Syntax	cec 6330	Extend the definition of a class to include equivalence class.
class [ A ] R
Syntax	cqs 6331	Extend the definition of a class to include quotient set.
class ( A /. R )
Definition	df-er 6332	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 6333 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 6352, ersymb 6346, and ertr 6347. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 2-Nov-2015.)
|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
Theorem	dfer2 6333*	Alternate definition of equivalence predicate. (Contributed by NM, 3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A <-> ( Rel R /\ dom R = A /\ A. x A. y A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
Definition	df-ec 6334	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 (i.e. when Er R; see dfer2 6333). 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 6335. (Contributed by NM, 23-Jul-1995.)
|- [ A ] R = ( R " { A } )
Theorem	dfec2 6335*	Alternate definition of R-coset of A. Definition 34 of [Suppes] p. 81. (Contributed by NM, 3-Jan-1997.) (Proof shortened by Mario Carneiro, 9-Jul-2014.)
|- ( A e. V -> [ A ] R = { y | A R y } )
Theorem	ecexg 6336	An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995.)
|- ( R e. B -> [ A ] R e. _V )
Theorem	ecexr 6337	An inhabited equivalence class implies the representative is a set. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( A e. [ B ] R -> B e. _V )
Definition	df-qs 6338*	Define quotient set. R is usually an equivalence relation. Definition of [Enderton] p. 58. (Contributed by NM, 23-Jul-1995.)
|- ( A /. R ) = { y | E. x e. A y = [ x ] R }
Theorem	ereq1 6339	Equality theorem for equivalence predicate. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( R = S -> ( R Er A <-> S Er A ) )
Theorem	ereq2 6340	Equality theorem for equivalence predicate. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( A = B -> ( R Er A <-> R Er B ) )
Theorem	errel 6341	An equivalence relation is a relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> Rel R )
Theorem	erdm 6342	The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> dom R = A )
Theorem	ercl 6343	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   =>    |- ( ph -> A e. X )
Theorem	ersym 6344	An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   =>    |- ( ph -> B R A )
Theorem	ercl2 6345	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   =>    |- ( ph -> B e. X )
Theorem	ersymb 6346	An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   =>    |- ( ph -> ( A R B <-> B R A ) )
Theorem	ertr 6347	An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   =>    |- ( ph -> ( ( A R B /\ B R C ) -> A R C ) )
Theorem	ertrd 6348	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	ertr2d 6349	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   &    |- ( ph -> B R C )   =>    |- ( ph -> C R A )
Theorem	ertr3d 6350	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> B R A )   &    |- ( ph -> B R C )   =>    |- ( ph -> A R C )
Theorem	ertr4d 6351	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   &    |- ( ph -> C R B )   =>    |- ( ph -> A R C )
Theorem	erref 6352	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.)
|- ( ph -> R Er X )   &    |- ( ph -> A e. X )   =>    |- ( ph -> A R A )
Theorem	ercnv 6353	The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> `' R = R )
Theorem	errn 6354	The range and domain of an equivalence relation are equal. (Contributed by Rodolfo Medina, 11-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> ran R = A )
Theorem	erssxp 6355	An equivalence relation is a subset of the cartesian product of the field. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> R C_ ( A X. A ) )
Theorem	erex 6356	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.)
|- ( R Er A -> ( A e. V -> R e. _V ) )
Theorem	erexb 6357	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.)
|- ( R Er A -> ( R e. _V <-> A e. _V ) )
Theorem	iserd 6358*	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.)
|- ( ph -> Rel R )   &    |- ( ( ph /\ x R y ) -> y R x )   &    |- ( ( ph /\ ( x R y /\ y R z ) ) -> x R z )   &    |- ( ph -> ( x e. A <-> x R x ) )   =>    |- ( ph -> R Er A )
Theorem	brdifun 6359	Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- R = ( ( X X. X ) \ ( .< u. `' .< ) )   =>    |- ( ( A e. X /\ B e. X ) -> ( A R B <-> -. ( A .< B \/ B .< A ) ) )
Theorem	swoer 6360*	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.)
|- R = ( ( X X. X ) \ ( .< u. `' .< ) )   &    |- ( ( ph /\ ( y e. X /\ z e. X ) ) -> ( y .< z -> -. z .< y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x .< y -> ( x .< z \/ z .< y ) ) )   =>    |- ( ph -> R Er X )
Theorem	swoord1 6361*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|- R = ( ( X X. X ) \ ( .< u. `' .< ) )   &    |- ( ( ph /\ ( y e. X /\ z e. X ) ) -> ( y .< z -> -. z .< y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x .< y -> ( x .< z \/ z .< y ) ) )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> A R B )   =>    |- ( ph -> ( A .< C <-> B .< C ) )
Theorem	swoord2 6362*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|- R = ( ( X X. X ) \ ( .< u. `' .< ) )   &    |- ( ( ph /\ ( y e. X /\ z e. X ) ) -> ( y .< z -> -. z .< y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x .< y -> ( x .< z \/ z .< y ) ) )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> A R B )   =>    |- ( ph -> ( C .< A <-> C .< B ) )
Theorem	eqerlem 6363*	Lemma for eqer 6364. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
|- ( x = y -> A = B )   &    |- R = { <. x , y >. | A = B }   =>    |- ( z R w <-> [_ z / x ]_ A = [_ w / x ]_ A )
Theorem	eqer 6364*	Equivalence relation involving equality of dependent classes A ( x ) and B ( y ). (Contributed by NM, 17-Mar-2008.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( x = y -> A = B )   &    |- R = { <. x , y >. | A = B }   =>    |- R Er _V
Theorem	ider 6365	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 6366	The empty set is an equivalence relation on the empty set. (Contributed by Mario Carneiro, 5-Sep-2015.)
|- (/) Er (/)
Theorem	eceq1 6367	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> [ A ] C = [ B ] C )
Theorem	eceq1d 6368	Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
|- ( ph -> A = B )   =>    |- ( ph -> [ A ] C = [ B ] C )
Theorem	eceq2 6369	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> [ C ] A = [ C ] B )
Theorem	elecg 6370	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ( A e. V /\ B e. W ) -> ( A e. [ B ] R <-> B R A ) )
Theorem	elec 6371	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.)
|- A e. _V   &    |- B e. _V   =>    |- ( A e. [ B ] R <-> B R A )
Theorem	relelec 6372	Membership in an equivalence class when R is a relation. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( Rel R -> ( A e. [ B ] R <-> B R A ) )
Theorem	ecss 6373	An equivalence class is a subset of the domain. (Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   =>    |- ( ph -> [ A ] R C_ X )
Theorem	ecdmn0m 6374*	A representative of an inhabited equivalence class belongs to the domain of the equivalence relation. (Contributed by Jim Kingdon, 21-Aug-2019.)
|- ( A e. dom R <-> E. x x e. [ A ] R )
Theorem	ereldm 6375	Equality of equivalence classes implies equivalence of domain membership. (Contributed by NM, 28-Jan-1996.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> [ A ] R = [ B ] R )   =>    |- ( ph -> ( A e. X <-> B e. X ) )
Theorem	erth 6376	Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
|- ( ph -> R Er X )   &    |- ( ph -> A e. X )   =>    |- ( ph -> ( A R B <-> [ A ] R = [ B ] R ) )
Theorem	erth2 6377	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.)
|- ( ph -> R Er X )   &    |- ( ph -> B e. X )   =>    |- ( ph -> ( A R B <-> [ A ] R = [ B ] R ) )
Theorem	erthi 6378	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.)
|- ( ph -> R Er X )   &    |- ( ph -> A R B )   =>    |- ( ph -> [ A ] R = [ B ] R )
Theorem	ecidsn 6379	An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.)
|- [ A ] _I = { A }
Theorem	qseq1 6380	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> ( A /. C ) = ( B /. C ) )
Theorem	qseq2 6381	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> ( C /. A ) = ( C /. B ) )
Theorem	elqsg 6382*	Closed form of elqs 6383. (Contributed by Rodolfo Medina, 12-Oct-2010.)
|- ( B e. V -> ( B e. ( A /. R ) <-> E. x e. A B = [ x ] R ) )
Theorem	elqs 6383*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|- B e. _V   =>    |- ( B e. ( A /. R ) <-> E. x e. A B = [ x ] R )
Theorem	elqsi 6384*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( B e. ( A /. R ) -> E. x e. A B = [ x ] R )
Theorem	ecelqsg 6385	Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( ( R e. V /\ B e. A ) -> [ B ] R e. ( A /. R ) )
Theorem	ecelqsi 6386	Membership of an equivalence class in a quotient set. (Contributed by NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- R e. _V   =>    |- ( B e. A -> [ B ] R e. ( A /. R ) )
Theorem	ecopqsi 6387	"Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996.)
|- R e. _V   &    |- S = ( ( A X. A ) /. R )   =>    |- ( ( B e. A /\ C e. A ) -> [ <. B , C >. ] R e. S )
Theorem	qsexg 6388	A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( A e. V -> ( A /. R ) e. _V )
Theorem	qsex 6389	A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|- A e. _V   =>    |- ( A /. R ) e. _V
Theorem	uniqs 6390	The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|- ( R e. V -> U. ( A /. R ) = ( R " A ) )
Theorem	qsss 6391	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.)
|- ( ph -> R Er A )   =>    |- ( ph -> ( A /. R ) C_ ~P A )
Theorem	uniqs2 6392	The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- ( ph -> R Er A )   &    |- ( ph -> R e. V )   =>    |- ( ph -> U. ( A /. R ) = A )
Theorem	snec 6393	The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- A e. _V   =>    |- { [ A ] R } = ( { A } /. R )
Theorem	ecqs 6394	Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.)
|- R e. _V   =>    |- [ A ] R = U. ( { A } /. R )
Theorem	ecid 6395	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.)
|- A e. _V   =>    |- [ A ] `' _E = A
Theorem	ecidg 6396	A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by Jim Kingdon, 8-Jan-2020.)
|- ( A e. V -> [ A ] `' _E = A )
Theorem	qsid 6397	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.)
|- ( A /. `' _E ) = A
Theorem	ectocld 6398*	Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- S = ( B /. R )   &    |- ( [ x ] R = A -> ( ph <-> ps ) )   &    |- ( ( ch /\ x e. B ) -> ph )   =>    |- ( ( ch /\ A e. S ) -> ps )
Theorem	ectocl 6399*	Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- S = ( B /. R )   &    |- ( [ x ] R = A -> ( ph <-> ps ) )   &    |- ( x e. B -> ph )   =>    |- ( A e. S -> ps )
Theorem	elqsn0m 6400*	An element of a quotient set is inhabited. (Contributed by Jim Kingdon, 21-Aug-2019.)
|- ( ( dom R = A /\ B e. ( A /. R ) ) -> E. x x e. B )