P. 30 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 2901-3000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ceqsex8v 2901*	Elimination of eight existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- D e. _V   &   |- E e. _V   &   |- F e. _V   &   |- G e. _V   &   |- H e. _V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   &   |- (w = D -> (th <-> ta))   &   |- (v = E -> (ta <-> et))   &   |- (u = F -> (et <-> ze))   &   |- (t = G -> (ze <-> si))   &   |- (s = H -> (si <-> rh))   =>   |- (E.xE.yE.zE.wE.vE.uE.tE.s(((x = A /\ y = B) /\ (z = C /\ w = D)) /\ ((v = E /\ u = F) /\ (t = G /\ s = H)) /\ ph) <-> rh)
Theorem	gencbvex 2902*	Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|- A e. _V   &   |- (A = y -> (ph <-> ps))   &   |- (A = y -> (ch <-> th))   &   |- (th <-> E.x(ch /\ A = y))   =>   |- (E.x(ch /\ ph) <-> E.y(th /\ ps))
Theorem	gencbvex2 2903*	Restatement of gencbvex 2902 with weaker hypotheses. (Contributed by Jeffrey Hankins, 6-Dec-2006.)
|- A e. _V   &   |- (A = y -> (ph <-> ps))   &   |- (A = y -> (ch <-> th))   &   |- (th -> E.x(ch /\ A = y))   =>   |- (E.x(ch /\ ph) <-> E.y(th /\ ps))
Theorem	gencbval 2904*	Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.)
|- A e. _V   &   |- (A = y -> (ph <-> ps))   &   |- (A = y -> (ch <-> th))   &   |- (th <-> E.x(ch /\ A = y))   =>   |- (A.x(ch -> ph) <-> A.y(th -> ps))
Theorem	sbhypf 2905*	Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf 3172. (Contributed by Raph Levien, 10-Apr-2004.)
|- F/xps   &   |- (x = A -> (ph <-> ps))   =>   |- (y = A -> ([y / x]ph <-> ps))
Theorem	vtoclgft 2906	Closed theorem form of vtoclgf 2914. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 12-Oct-2016.)
|- ((( F/_xA /\ F/xps) /\ (A.x(x = A -> (ph <-> ps)) /\ A.xph) /\ A e. V) -> ps)
Theorem	vtocldf 2907	Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.)
|- (ph -> A e. V)   &   |- ((ph /\ x = A) -> (ps <-> ch))   &   |- (ph -> ps)   &   |- F/xph   &   |- (ph -> F/_xA)   &   |- (ph -> F/xch)   =>   |- (ph -> ch)
Theorem	vtocld 2908*	Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.)
|- (ph -> A e. V)   &   |- ((ph /\ x = A) -> (ps <-> ch))   &   |- (ph -> ps)   =>   |- (ph -> ch)
Theorem	vtoclf 2909*	Implicit substitution of a class for a setvar variable. This is a generalization of chvar 1986. (Contributed by NM, 30-Aug-1993.)
|- F/xps   &   |- A e. _V   &   |- (x = A -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtocl 2910*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.)
|- A e. _V   &   |- (x = A -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtocl2 2911*	Implicit substitution of classes for setvar variables. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|- A e. _V   &   |- B e. _V   &   |- ((x = A /\ y = B) -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtocl3 2912*	Implicit substitution of classes for setvar variables. (Contributed by NM, 3-Jun-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- ((x = A /\ y = B /\ z = C) -> (ph <-> ps))   &   |- ph   =>   |- ps
Theorem	vtoclb 2913*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 23-Dec-1993.)
|- A e. _V   &   |- (x = A -> (ph <-> ch))   &   |- (x = A -> (ps <-> th))   &   |- (ph <-> ps)   =>   |- (ch <-> th)
Theorem	vtoclgf 2914	Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) (Proof shortened by Mario Carneiro, 10-Oct-2016.)
|- F/_xA   &   |- F/xps   &   |- (x = A -> (ph <-> ps))   &   |- ph   =>   |- (A e. V -> ps)
Theorem	vtoclg 2915*	Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.)
|- (x = A -> (ph <-> ps))   &   |- ph   =>   |- (A e. V -> ps)
Theorem	vtoclbg 2916*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)
|- (x = A -> (ph <-> ch))   &   |- (x = A -> (ps <-> th))   &   |- (ph <-> ps)   =>   |- (A e. V -> (ch <-> th))
Theorem	vtocl2gf 2917	Implicit substitution of a class for a setvar variable. (Contributed by NM, 25-Apr-1995.)
|- F/_xA   &   |- F/_yA   &   |- F/_yB   &   |- F/xps   &   |- F/ych   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- ph   =>   |- ((A e. V /\ B e. W) -> ch)
Theorem	vtocl3gf 2918	Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
|- F/_xA   &   |- F/_yA   &   |- F/_zA   &   |- F/_yB   &   |- F/_zB   &   |- F/_zC   &   |- F/xps   &   |- F/ych   &   |- F/zth   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   &   |- ph   =>   |- ((A e. V /\ B e. W /\ C e. X) -> th)
Theorem	vtocl2g 2919*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.)
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- ph   =>   |- ((A e. V /\ B e. W) -> ch)
Theorem	vtoclgaf 2920*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.)
|- F/_xA   &   |- F/xps   &   |- (x = A -> (ph <-> ps))   &   |- (x e. B -> ph)   =>   |- (A e. B -> ps)
Theorem	vtoclga 2921*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.)
|- (x = A -> (ph <-> ps))   &   |- (x e. B -> ph)   =>   |- (A e. B -> ps)
Theorem	vtocl2gaf 2922*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 10-Aug-2013.)
|- F/_xA   &   |- F/_yA   &   |- F/_yB   &   |- F/xps   &   |- F/ych   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- ((x e. C /\ y e. D) -> ph)   =>   |- ((A e. C /\ B e. D) -> ch)
Theorem	vtocl2ga 2923*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.)
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- ((x e. C /\ y e. D) -> ph)   =>   |- ((A e. C /\ B e. D) -> ch)
Theorem	vtocl3gaf 2924*	Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 11-Oct-2016.)
|- F/_xA   &   |- F/_yA   &   |- F/_zA   &   |- F/_yB   &   |- F/_zB   &   |- F/_zC   &   |- F/xps   &   |- F/ych   &   |- F/zth   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   &   |- ((x e. R /\ y e. S /\ z e. T) -> ph)   =>   |- ((A e. R /\ B e. S /\ C e. T) -> th)
Theorem	vtocl3ga 2925*	Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 20-Aug-1995.)
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   &   |- ((x e. D /\ y e. R /\ z e. S) -> ph)   =>   |- ((A e. D /\ B e. R /\ C e. S) -> th)
Theorem	vtocleg 2926*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Jan-2004.)
|- (x = A -> ph)   =>   |- (A e. V -> ph)
Theorem	vtoclegft 2927*	Implicit substitution of a class for a setvar variable. (Closed theorem version of vtoclef 2928.) (Contributed by NM, 7-Nov-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
|- ((A e. B /\ F/xph /\ A.x(x = A -> ph)) -> ph)
Theorem	vtoclef 2928*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 18-Aug-1993.)
|- F/xph   &   |- A e. _V   &   |- (x = A -> ph)   =>   |- ph
Theorem	vtocle 2929*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 9-Sep-1993.)
|- A e. _V   &   |- (x = A -> ph)   =>   |- ph
Theorem	vtoclri 2930*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Nov-1994.)
|- (x = A -> (ph <-> ps))   &   |- A.x e. B ph   =>   |- (A e. B -> ps)
Theorem	spcimgft 2931	A closed version of spcimgf 2933. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- F/xps   &   |- F/_xA   =>   |- (A.x(x = A -> (ph -> ps)) -> (A e. B -> (A.xph -> ps)))
Theorem	spcgft 2932	A closed version of spcgf 2935. (Contributed by Andrew Salmon, 6-Jun-2011.) (Revised by Mario Carneiro, 4-Jan-2017.)
|- F/xps   &   |- F/_xA   =>   |- (A.x(x = A -> (ph <-> ps)) -> (A e. B -> (A.xph -> ps)))
Theorem	spcimgf 2933	Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- F/_xA   &   |- F/xps   &   |- (x = A -> (ph -> ps))   =>   |- (A e. V -> (A.xph -> ps))
Theorem	spcimegf 2934	Existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- F/_xA   &   |- F/xps   &   |- (x = A -> (ps -> ph))   =>   |- (A e. V -> (ps -> E.xph))
Theorem	spcgf 2935	Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 2-Feb-1997.) (Revised by Andrew Salmon, 12-Aug-2011.)
|- F/_xA   &   |- F/xps   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. V -> (A.xph -> ps))
Theorem	spcegf 2936	Existential specialization, using implicit substitution. (Contributed by NM, 2-Feb-1997.)
|- F/_xA   &   |- F/xps   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. V -> (ps -> E.xph))
Theorem	spcimdv 2937*	Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- (ph -> A e. B)   &   |- ((ph /\ x = A) -> (ps -> ch))   =>   |- (ph -> (A.xps -> ch))
Theorem	spcdv 2938*	Rule of specialization, using implicit substitution. Analogous to rspcdv 2959. (Contributed by David Moews, 1-May-2017.)
|- (ph -> A e. B)   &   |- ((ph /\ x = A) -> (ps <-> ch))   =>   |- (ph -> (A.xps -> ch))
Theorem	spcimedv 2939*	Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- (ph -> A e. B)   &   |- ((ph /\ x = A) -> (ch -> ps))   =>   |- (ph -> (ch -> E.xps))
Theorem	spcgv 2940*	Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.)
|- (x = A -> (ph <-> ps))   =>   |- (A e. V -> (A.xph -> ps))
Theorem	spcegv 2941*	Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.)
|- (x = A -> (ph <-> ps))   =>   |- (A e. V -> (ps -> E.xph))
Theorem	spc2egv 2942*	Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by NM, 3-Aug-1995.)
|- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- ((A e. V /\ B e. W) -> (ps -> E.xE.yph))
Theorem	spc2gv 2943*	Specialization with 2 quantifiers, using implicit substitution. (Contributed by NM, 27-Apr-2004.)
|- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- ((A e. V /\ B e. W) -> (A.xA.yph -> ps))
Theorem	spc3egv 2944*	Existential specialization with 3 quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.)
|- ((x = A /\ y = B /\ z = C) -> (ph <-> ps))   =>   |- ((A e. V /\ B e. W /\ C e. X) -> (ps -> E.xE.yE.zph))
Theorem	spc3gv 2945*	Specialization with 3 quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.)
|- ((x = A /\ y = B /\ z = C) -> (ph <-> ps))   =>   |- ((A e. V /\ B e. W /\ C e. X) -> (A.xA.yA.zph -> ps))
Theorem	spcv 2946*	Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.)
|- A e. _V   &   |- (x = A -> (ph <-> ps))   =>   |- (A.xph -> ps)
Theorem	spcev 2947*	Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
|- A e. _V   &   |- (x = A -> (ph <-> ps))   =>   |- (ps -> E.xph)
Theorem	spc2ev 2948*	Existential specialization, using implicit substitution. (Contributed by NM, 3-Aug-1995.)
|- A e. _V   &   |- B e. _V   &   |- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- (ps -> E.xE.yph)
Theorem	rspct 2949*	A closed version of rspc 2950. (Contributed by Andrew Salmon, 6-Jun-2011.)
|- F/xps   =>   |- (A.x(x = A -> (ph <-> ps)) -> (A e. B -> (A.x e. B ph -> ps)))
Theorem	rspc 2950*	Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
|- F/xps   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A.x e. B ph -> ps))
Theorem	rspce 2951*	Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro, 11-Oct-2016.)
|- F/xps   &   |- (x = A -> (ph <-> ps))   =>   |- ((A e. B /\ ps) -> E.x e. B ph)
Theorem	rspcv 2952*	Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A.x e. B ph -> ps))
Theorem	rspccv 2953*	Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.)
|- (x = A -> (ph <-> ps))   =>   |- (A.x e. B ph -> (A e. B -> ps))
Theorem	rspcva 2954*	Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)
|- (x = A -> (ph <-> ps))   =>   |- ((A e. B /\ A.x e. B ph) -> ps)
Theorem	rspccva 2955*	Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|- (x = A -> (ph <-> ps))   =>   |- ((A.x e. B ph /\ A e. B) -> ps)
Theorem	rspcev 2956*	Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
|- (x = A -> (ph <-> ps))   =>   |- ((A e. B /\ ps) -> E.x e. B ph)
Theorem	rspcimdv 2957*	Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- (ph -> A e. B)   &   |- ((ph /\ x = A) -> (ps -> ch))   =>   |- (ph -> (A.x e. B ps -> ch))
Theorem	rspcimedv 2958*	Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- (ph -> A e. B)   &   |- ((ph /\ x = A) -> (ch -> ps))   =>   |- (ph -> (ch -> E.x e. B ps))
Theorem	rspcdv 2959*	Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
|- (ph -> A e. B)   &   |- ((ph /\ x = A) -> (ps <-> ch))   =>   |- (ph -> (A.x e. B ps -> ch))
Theorem	rspcedv 2960*	Restricted existential specialization, using implicit substitution. (Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
|- (ph -> A e. B)   &   |- ((ph /\ x = A) -> (ps <-> ch))   =>   |- (ph -> (ch -> E.x e. B ps))
Theorem	rspc2 2961*	2-variable restricted specialization, using implicit substitution. (Contributed by NM, 9-Nov-2012.)
|- F/xch   &   |- F/yps   &   |- (x = A -> (ph <-> ch))   &   |- (y = B -> (ch <-> ps))   =>   |- ((A e. C /\ B e. D) -> (A.x e. C A.y e. D ph -> ps))
Theorem	rspc2v 2962*	2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.)
|- (x = A -> (ph <-> ch))   &   |- (y = B -> (ch <-> ps))   =>   |- ((A e. C /\ B e. D) -> (A.x e. C A.y e. D ph -> ps))
Theorem	rspc2va 2963*	2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.)
|- (x = A -> (ph <-> ch))   &   |- (y = B -> (ch <-> ps))   =>   |- (((A e. C /\ B e. D) /\ A.x e. C A.y e. D ph) -> ps)
Theorem	rspc2ev 2964*	2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)
|- (x = A -> (ph <-> ch))   &   |- (y = B -> (ch <-> ps))   =>   |- ((A e. C /\ B e. D /\ ps) -> E.x e. C E.y e. D ph)
Theorem	rspc3v 2965*	3-variable restricted specialization, using implicit substitution. (Contributed by NM, 10-May-2005.)
|- (x = A -> (ph <-> ch))   &   |- (y = B -> (ch <-> th))   &   |- (z = C -> (th <-> ps))   =>   |- ((A e. R /\ B e. S /\ C e. T) -> (A.x e. R A.y e. S A.z e. T ph -> ps))
Theorem	rspc3ev 2966*	3-variable restricted existentional specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012.)
|- (x = A -> (ph <-> ch))   &   |- (y = B -> (ch <-> th))   &   |- (z = C -> (th <-> ps))   =>   |- (((A e. R /\ B e. S /\ C e. T) /\ ps) -> E.x e. R E.y e. S E.z e. T ph)
Theorem	eqvinc 2967*	A variable introduction law for class equality. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|- A e. _V   =>   |- (A = B <-> E.x(x = A /\ x = B))
Theorem	eqvincf 2968	A variable introduction law for class equality, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Sep-2003.)
|- F/_xA   &   |- F/_xB   &   |- A e. _V   =>   |- (A = B <-> E.x(x = A /\ x = B))
Theorem	alexeq 2969*	Two ways to express substitution of A for x in ph. (Contributed by NM, 2-Mar-1995.)
|- A e. _V   =>   |- (A.x(x = A -> ph) <-> E.x(x = A /\ ph))
Theorem	ceqex 2970*	Equality implies equivalence with substitution. (Contributed by NM, 2-Mar-1995.)
|- (x = A -> (ph <-> E.x(x = A /\ ph)))
Theorem	ceqsexg 2971*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 11-Oct-2004.)
|- F/xps   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. V -> (E.x(x = A /\ ph) <-> ps))
Theorem	ceqsexgv 2972*	Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 29-Dec-1996.)
|- (x = A -> (ph <-> ps))   =>   |- (A e. V -> (E.x(x = A /\ ph) <-> ps))
Theorem	ceqsrexv 2973*	Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004.)
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (E.x e. B (x = A /\ ph) <-> ps))
Theorem	ceqsrexbv 2974*	Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by Mario Carneiro, 14-Mar-2014.)
|- (x = A -> (ph <-> ps))   =>   |- (E.x e. B (x = A /\ ph) <-> (A e. B /\ ps))
Theorem	ceqsrex2v 2975*	Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 29-Oct-2005.)
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   =>   |- ((A e. C /\ B e. D) -> (E.x e. C E.y e. D ((x = A /\ y = B) /\ ph) <-> ch))
Theorem	clel2 2976*	An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.)
|- A e. _V   =>   |- (A e. B <-> A.x(x = A -> x e. B))
Theorem	clel3g 2977*	An alternate definition of class membership when the class is a set. (Contributed by NM, 13-Aug-2005.)
|- (B e. V -> (A e. B <-> E.x(x = B /\ A e. x)))
Theorem	clel3 2978*	An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.)
|- B e. _V   =>   |- (A e. B <-> E.x(x = B /\ A e. x))
Theorem	clel4 2979*	An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.)
|- B e. _V   =>   |- (A e. B <-> A.x(x = B -> A e. x))
Theorem	pm13.183 2980*	Compare theorem *13.183 in [WhiteheadRussell] p. 178. Only A is required to be a set. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- (A e. V -> (A = B <-> A.z(z = A <-> z = B)))
Theorem	rr19.3v 2981*	Restricted quantifier version of Theorem 19.3 of [Margaris] p. 89. We don't need the nonempty class condition of r19.3rzv 3644 when there is an outer quantifier. (Contributed by NM, 25-Oct-2012.)
|- (A.x e. A A.y e. A ph <-> A.x e. A ph)
Theorem	rr19.28v 2982*	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. We don't need the nonempty class condition of r19.28zv 3646 when there is an outer quantifier. (Contributed by NM, 29-Oct-2012.)
|- (A.x e. A A.y e. A (ph /\ ps) <-> A.x e. A (ph /\ A.y e. A ps))
Theorem	elabgt 2983*	Membership in a class abstraction, using implicit substitution. (Closed theorem version of elabg 2987.) (Contributed by NM, 7-Nov-2005.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|- ((A e. B /\ A.x(x = A -> (ph <-> ps))) -> (A e. {x | ph} <-> ps))
Theorem	elabgf 2984	Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) (Revised by Mario Carneiro, 12-Oct-2016.)
|- F/_xA   &   |- F/xps   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A e. {x | ph} <-> ps))
Theorem	elabf 2985*	Membership in a class abstraction, using implicit substitution. (Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro, 12-Oct-2016.)
|- F/xps   &   |- A e. _V   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. {x | ph} <-> ps)
Theorem	elab 2986*	Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 1-Aug-1994.)
|- A e. _V   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. {x | ph} <-> ps)
Theorem	elabg 2987*	Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.)
|- (x = A -> (ph <-> ps))   =>   |- (A e. V -> (A e. {x | ph} <-> ps))
Theorem	elab2g 2988*	Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
|- (x = A -> (ph <-> ps))   &   |- B = {x | ph}   =>   |- (A e. V -> (A e. B <-> ps))
Theorem	elab2 2989*	Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
|- A e. _V   &   |- (x = A -> (ph <-> ps))   &   |- B = {x | ph}   =>   |- (A e. B <-> ps)
Theorem	elab4g 2990*	Membership in a class abstraction, using implicit substitution. (Contributed by NM, 17-Oct-2012.)
|- (x = A -> (ph <-> ps))   &   |- B = {x | ph}   =>   |- (A e. B <-> (A e. _V /\ ps))
Theorem	elab3gf 2991	Membership in a class abstraction, with a weaker antecedent than elabgf 2984. (Contributed by NM, 6-Sep-2011.)
|- F/_xA   &   |- F/xps   &   |- (x = A -> (ph <-> ps))   =>   |- ((ps -> A e. B) -> (A e. {x | ph} <-> ps))
Theorem	elab3g 2992*	Membership in a class abstraction, with a weaker antecedent than elabg 2987. (Contributed by NM, 29-Aug-2006.)
|- (x = A -> (ph <-> ps))   =>   |- ((ps -> A e. B) -> (A e. {x | ph} <-> ps))
Theorem	elab3 2993*	Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.)
|- (ps -> A e. _V)   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. {x | ph} <-> ps)
Theorem	elrabf 2994	Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.)
|- F/_xA   &   |- F/_xB   &   |- F/xps   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. {x e. B | ph} <-> (A e. B /\ ps))
Theorem	elrab 2995*	Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.)
|- (x = A -> (ph <-> ps))   =>   |- (A e. {x e. B | ph} <-> (A e. B /\ ps))
Theorem	elrab3 2996*	Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006.)
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> (A e. {x e. B | ph} <-> ps))
Theorem	elrab2 2997*	Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.)
|- (x = A -> (ph <-> ps))   &   |- C = {x e. B | ph}   =>   |- (A e. C <-> (A e. B /\ ps))
Theorem	ralab 2998*	Universal quantification over a class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- (y = x -> (ph <-> ps))   =>   |- (A.x e. {y | ph}ch <-> A.x(ps -> ch))
Theorem	ralrab 2999*	Universal quantification over a restricted class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- (y = x -> (ph <-> ps))   =>   |- (A.x e. {y e. A | ph}ch <-> A.x e. A (ps -> ch))
Theorem	rexab 3000*	Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 23-Jan-2014.) (Revised by Mario Carneiro, 3-Sep-2015.)
|- (y = x -> (ph <-> ps))   =>   |- (E.x e. {y | ph}ch <-> E.x(ps /\ ch))