P. 66 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6501-6600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	3onn 6501	The ordinal 3 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 3o e. om
Theorem	4onn 6502	The ordinal 4 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 4o e. om
Theorem	2ssom 6503	The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.)
|- 2o C_ om
Theorem	nnm1 6504	Multiply an element of om by 1o. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( A .o 1o ) = A )
Theorem	nnm2 6505	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 6506	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 6507*	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 6508*	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 6509	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.25  Equivalence relations and classes
Syntax	wer 6510	Extend the definition of a wff to include the equivalence predicate.
wff R Er A
Syntax	cec 6511	Extend the definition of a class to include equivalence class.
class [ A ] R
Syntax	cqs 6512	Extend the definition of a class to include quotient set.
class ( A /. R )
Definition	df-er 6513	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 6514 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 6533, ersymb 6527, and ertr 6528. (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 6514*	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 6515	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 6514). 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 6516. (Contributed by NM, 23-Jul-1995.)
|- [ A ] R = ( R " { A } )
Theorem	dfec2 6516*	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 6517	An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995.)
|- ( R e. B -> [ A ] R e. _V )
Theorem	ecexr 6518	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 6519*	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 6520	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 6521	Equality theorem for equivalence predicate. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( A = B -> ( R Er A <-> R Er B ) )
Theorem	errel 6522	An equivalence relation is a relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> Rel R )
Theorem	erdm 6523	The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> dom R = A )
Theorem	ercl 6524	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 6525	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 6526	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 6527	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 6528	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 6529	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 6530	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 6531	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 6532	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 6533	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 6534	The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( R Er A -> `' R = R )
Theorem	errn 6535	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 6536	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 6537	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 6538	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 6539*	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 6540	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 6541*	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 6542*	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 6543*	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 6544*	Lemma for eqer 6545. (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 6545*	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 6546	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 6547	The empty set is an equivalence relation on the empty set. (Contributed by Mario Carneiro, 5-Sep-2015.)
|- (/) Er (/)
Theorem	eceq1 6548	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> [ A ] C = [ B ] C )
Theorem	eceq1d 6549	Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
|- ( ph -> A = B )   =>    |- ( ph -> [ A ] C = [ B ] C )
Theorem	eceq2 6550	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> [ C ] A = [ C ] B )
Theorem	elecg 6551	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 6552	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 6553	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 6554	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 6555*	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 6556	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 6557	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 6558	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 6559	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 6560	An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.)
|- [ A ] _I = { A }
Theorem	qseq1 6561	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> ( A /. C ) = ( B /. C ) )
Theorem	qseq2 6562	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( A = B -> ( C /. A ) = ( C /. B ) )
Theorem	elqsg 6563*	Closed form of elqs 6564. (Contributed by Rodolfo Medina, 12-Oct-2010.)
|- ( B e. V -> ( B e. ( A /. R ) <-> E. x e. A B = [ x ] R ) )
Theorem	elqs 6564*	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 6565*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
|- ( B e. ( A /. R ) -> E. x e. A B = [ x ] R )
Theorem	ecelqsg 6566	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 6567	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 6568	"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 6569	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 6570	A quotient set exists. (Contributed by NM, 14-Aug-1995.)
|- A e. _V   =>    |- ( A /. R ) e. _V
Theorem	uniqs 6571	The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
|- ( R e. V -> U. ( A /. R ) = ( R " A ) )
Theorem	qsss 6572	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 6573	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 6574	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 6575	Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.)
|- R e. _V   =>    |- [ A ] R = U. ( { A } /. R )
Theorem	ecid 6576	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 6577	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 6578	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 6579*	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 6580*	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 6581*	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 )
Theorem	elqsn0 6582	A quotient set doesn't contain the empty set. (Contributed by NM, 24-Aug-1995.)
|- ( ( dom R = A /\ B e. ( A /. R ) ) -> B =/= (/) )
Theorem	ecelqsdm 6583	Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995.)
|- ( ( dom R = A /\ [ B ] R e. ( A /. R ) ) -> B e. A )
Theorem	xpider 6584	A square Cartesian product is an equivalence relation (in general it's not a poset). (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( A X. A ) Er A
Theorem	iinerm 6585*	The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( ( E. y y e. A /\ A. x e. A R Er B ) -> |^|_ x e. A R Er B )
Theorem	riinerm 6586*	The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( ( E. y y e. A /\ A. x e. A R Er B ) -> ( ( B X. B ) i^i |^|_ x e. A R ) Er B )
Theorem	erinxp 6587	A restricted equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ph -> R Er A )   &    |- ( ph -> B C_ A )   =>    |- ( ph -> ( R i^i ( B X. B ) ) Er B )
Theorem	ecinxp 6588	Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015.)
|- ( ( ( R " A ) C_ A /\ B e. A ) -> [ B ] R = [ B ] ( R i^i ( A X. A ) ) )
Theorem	qsinxp 6589	Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
|- ( ( R " A ) C_ A -> ( A /. R ) = ( A /. ( R i^i ( A X. A ) ) ) )
Theorem	qsel 6590	If an element of a quotient set contains a given element, it is equal to the equivalence class of the element. (Contributed by Mario Carneiro, 12-Aug-2015.)
|- ( ( R Er X /\ B e. ( A /. R ) /\ C e. B ) -> B = [ C ] R )
Theorem	qliftlem 6591*	F, a function lift, is a subset of R X. S. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ( ph /\ x e. X ) -> [ x ] R e. ( X /. R ) )
Theorem	qliftrel 6592*	F, a function lift, is a subset of R X. S. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ph -> F C_ ( ( X /. R ) X. Y ) )
Theorem	qliftel 6593*	Elementhood in the relation F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ph -> ( [ C ] R F D <-> E. x e. X ( C R x /\ D = A ) ) )
Theorem	qliftel1 6594*	Elementhood in the relation F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ( ph /\ x e. X ) -> [ x ] R F A )
Theorem	qliftfun 6595*	The function F is the unique function defined by F ` [ x ] = A, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   &    |- ( x = y -> A = B )   =>    |- ( ph -> ( Fun F <-> A. x A. y ( x R y -> A = B ) ) )
Theorem	qliftfund 6596*	The function F is the unique function defined by F ` [ x ] = A, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   &    |- ( x = y -> A = B )   &    |- ( ( ph /\ x R y ) -> A = B )   =>    |- ( ph -> Fun F )
Theorem	qliftfuns 6597*	The function F is the unique function defined by F ` [ x ] = A, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ph -> ( Fun F <-> A. y A. z ( y R z -> [_ y / x ]_ A = [_ z / x ]_ A ) ) )
Theorem	qliftf 6598*	The domain and range of the function F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   =>    |- ( ph -> ( Fun F <-> F : ( X /. R ) --> Y ) )
Theorem	qliftval 6599*	The value of the function F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. [ x ] R , A >. )   &    |- ( ( ph /\ x e. X ) -> A e. Y )   &    |- ( ph -> R Er X )   &    |- ( ph -> X e. _V )   &    |- ( x = C -> A = B )   &    |- ( ph -> Fun F )   =>    |- ( ( ph /\ C e. X ) -> ( F ` [ C ] R ) = B )
Theorem	ecoptocl 6600*	Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 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 )