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	gencbvex 2901*	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 2902*	Restatement of gencbvex 2901 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 2903*	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 2904*	Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf 3171. (Contributed by Raph Levien, 10-Apr-2004.)
|- F/xps   &   |- (x = A -> (ph <-> ps))   =>   |- (y = A -> ([y / x]ph <-> ps))
Theorem	vtoclgft 2905	Closed theorem form of vtoclgf 2913. (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 2906	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 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)   =>   |- (ph -> ch)
Theorem	vtoclf 2908*	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 2909*	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 2910*	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 2911*	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 2912*	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 2913	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 2914*	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 2915*	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 2916	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 2917	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 2918*	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 2919*	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 2920*	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 2921*	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 2922*	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 2923*	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 2924*	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 2925*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Jan-2004.)
|- (x = A -> ph)   =>   |- (A e. V -> ph)
Theorem	vtoclegft 2926*	Implicit substitution of a class for a setvar variable. (Closed theorem version of vtoclef 2927.) (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 2927*	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 2928*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 9-Sep-1993.)
|- A e. _V   &   |- (x = A -> ph)   =>   |- ph
Theorem	vtoclri 2929*	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 2930	A closed version of spcimgf 2932. (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 2931	A closed version of spcgf 2934. (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 2932	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 2933	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 2934	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 2935	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 2936*	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 2937*	Rule of specialization, using implicit substitution. Analogous to rspcdv 2958. (Contributed by David Moews, 1-May-2017.)
|- (ph -> A e. B)   &   |- ((ph /\ x = A) -> (ps <-> ch))   =>   |- (ph -> (A.xps -> ch))
Theorem	spcimedv 2938*	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 2939*	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 2940*	Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.)
|- (x = A -> (ph <-> ps))   =>   |- (A e. V -> (ps -> E.xph))
Theorem	spc2egv 2941*	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 2942*	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 2943*	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 2944*	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 2945*	Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.)
|- A e. _V   &   |- (x = A -> (ph <-> ps))   =>   |- (A.xph -> ps)
Theorem	spcev 2946*	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 2947*	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 2948*	A closed version of rspc 2949. (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 2949*	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 2950*	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 2951*	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 2952*	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 2953*	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 2954*	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 2955*	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 2956*	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 2957*	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 2958*	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 2959*	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 2960*	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 2961*	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 2962*	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 2963*	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 2964*	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 2965*	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 2966*	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 2967	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 2968*	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 2969*	Equality implies equivalence with substitution. (Contributed by NM, 2-Mar-1995.)
|- (x = A -> (ph <-> E.x(x = A /\ ph)))
Theorem	ceqsexg 2970*	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 2971*	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 2972*	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 2973*	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 2974*	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 2975*	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 2976*	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 2977*	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 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 <-> A.x(x = B -> A e. x))
Theorem	pm13.183 2979*	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 2980*	Restricted quantifier version of Theorem 19.3 of [Margaris] p. 89. We don't need the nonempty class condition of r19.3rzv 3643 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 2981*	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. We don't need the nonempty class condition of r19.28zv 3645 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 2982*	Membership in a class abstraction, using implicit substitution. (Closed theorem version of elabg 2986.) (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 2983	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 2984*	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 2985*	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 2986*	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 2987*	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 2988*	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 2989*	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 2990	Membership in a class abstraction, with a weaker antecedent than elabgf 2983. (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 2991*	Membership in a class abstraction, with a weaker antecedent than elabg 2986. (Contributed by NM, 29-Aug-2006.)
|- (x = A -> (ph <-> ps))   =>   |- ((ps -> A e. B) -> (A e. {x | ph} <-> ps))
Theorem	elab3 2992*	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 2993	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 2994*	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 2995*	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 2996*	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 2997*	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 2998*	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 2999*	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))
Theorem	rexrab 3000*	Existential quantification over a class abstraction. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Mario Carneiro, 3-Sep-2015.)
|- (y = x -> (ph <-> ps))   =>   |- (E.x e. {y e. A | ph}ch <-> E.x e. A (ps /\ ch))