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 ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ D ∈ V    &   ⊢ E ∈ V    &   ⊢ F ∈ V    &   ⊢ G ∈ V    &   ⊢ H ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (z = C → (χ ↔ θ))    &   ⊢ (w = D → (θ ↔ τ))    &   ⊢ (v = E → (τ ↔ η))    &   ⊢ (u = F → (η ↔ ζ))    &   ⊢ (t = G → (ζ ↔ σ))    &   ⊢ (s = H → (σ ↔ ρ))    ⇒   ⊢ (∃x∃y∃z∃w∃v∃u∃t∃s(((x = A ∧ y = B) ∧ (z = C ∧ w = D)) ∧ ((v = E ∧ u = F) ∧ (t = G ∧ s = H)) ∧ φ) ↔ ρ)
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 ∈ V    &   ⊢ (A = y → (φ ↔ ψ))    &   ⊢ (A = y → (χ ↔ θ))    &   ⊢ (θ ↔ ∃x(χ ∧ A = y))    ⇒   ⊢ (∃x(χ ∧ φ) ↔ ∃y(θ ∧ ψ))
Theorem	gencbvex2 2903*	Restatement of gencbvex 2902 with weaker hypotheses. (Contributed by Jeffrey Hankins, 6-Dec-2006.)
⊢ A ∈ V    &   ⊢ (A = y → (φ ↔ ψ))    &   ⊢ (A = y → (χ ↔ θ))    &   ⊢ (θ → ∃x(χ ∧ A = y))    ⇒   ⊢ (∃x(χ ∧ φ) ↔ ∃y(θ ∧ ψ))
Theorem	gencbval 2904*	Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.)
⊢ A ∈ V    &   ⊢ (A = y → (φ ↔ ψ))    &   ⊢ (A = y → (χ ↔ θ))    &   ⊢ (θ ↔ ∃x(χ ∧ A = y))    ⇒   ⊢ (∀x(χ → φ) ↔ ∀y(θ → ψ))
Theorem	sbhypf 2905*	Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf 3172. (Contributed by Raph Levien, 10-Apr-2004.)
⊢ Ⅎxψ    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (y = A → ([y / x]φ ↔ ψ))
Theorem	vtoclgft 2906	Closed theorem form of vtoclgf 2914. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ (((ℲxA ∧ Ⅎxψ) ∧ (∀x(x = A → (φ ↔ ψ)) ∧ ∀xφ) ∧ A ∈ V) → ψ)
Theorem	vtocldf 2907	Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.)
⊢ (φ → A ∈ V)    &   ⊢ ((φ ∧ x = A) → (ψ ↔ χ))    &   ⊢ (φ → ψ)    &   ⊢ Ⅎxφ    &   ⊢ (φ → ℲxA)    &   ⊢ (φ → Ⅎxχ)    ⇒   ⊢ (φ → χ)
Theorem	vtocld 2908*	Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.)
⊢ (φ → A ∈ V)    &   ⊢ ((φ ∧ x = A) → (ψ ↔ χ))    &   ⊢ (φ → ψ)    ⇒   ⊢ (φ → χ)
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.)
⊢ Ⅎxψ    &   ⊢ A ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ φ    ⇒   ⊢ ψ
Theorem	vtocl 2910*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.)
⊢ A ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ φ    ⇒   ⊢ ψ
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 ∈ V    &   ⊢ B ∈ V    &   ⊢ ((x = A ∧ y = B) → (φ ↔ ψ))    &   ⊢ φ    ⇒   ⊢ ψ
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 ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    &   ⊢ ((x = A ∧ y = B ∧ z = C) → (φ ↔ ψ))    &   ⊢ φ    ⇒   ⊢ ψ
Theorem	vtoclb 2913*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 23-Dec-1993.)
⊢ A ∈ V    &   ⊢ (x = A → (φ ↔ χ))    &   ⊢ (x = A → (ψ ↔ θ))    &   ⊢ (φ ↔ ψ)    ⇒   ⊢ (χ ↔ θ)
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.)
⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ φ    ⇒   ⊢ (A ∈ V → ψ)
Theorem	vtoclg 2915*	Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ φ    ⇒   ⊢ (A ∈ V → ψ)
Theorem	vtoclbg 2916*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)
⊢ (x = A → (φ ↔ χ))    &   ⊢ (x = A → (ψ ↔ θ))    &   ⊢ (φ ↔ ψ)    ⇒   ⊢ (A ∈ V → (χ ↔ θ))
Theorem	vtocl2gf 2917	Implicit substitution of a class for a setvar variable. (Contributed by NM, 25-Apr-1995.)
⊢ ℲxA    &   ⊢ ℲyA    &   ⊢ ℲyB    &   ⊢ Ⅎxψ    &   ⊢ Ⅎyχ    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ φ    ⇒   ⊢ ((A ∈ V ∧ B ∈ W) → χ)
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.)
⊢ ℲxA    &   ⊢ ℲyA    &   ⊢ ℲzA    &   ⊢ ℲyB    &   ⊢ ℲzB    &   ⊢ ℲzC    &   ⊢ Ⅎxψ    &   ⊢ Ⅎyχ    &   ⊢ Ⅎzθ    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (z = C → (χ ↔ θ))    &   ⊢ φ    ⇒   ⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) → θ)
Theorem	vtocl2g 2919*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ φ    ⇒   ⊢ ((A ∈ V ∧ B ∈ W) → χ)
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.)
⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (x ∈ B → φ)    ⇒   ⊢ (A ∈ B → ψ)
Theorem	vtoclga 2921*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (x ∈ B → φ)    ⇒   ⊢ (A ∈ B → ψ)
Theorem	vtocl2gaf 2922*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 10-Aug-2013.)
⊢ ℲxA    &   ⊢ ℲyA    &   ⊢ ℲyB    &   ⊢ Ⅎxψ    &   ⊢ Ⅎyχ    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ ((x ∈ C ∧ y ∈ D) → φ)    ⇒   ⊢ ((A ∈ C ∧ B ∈ D) → χ)
Theorem	vtocl2ga 2923*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ ((x ∈ C ∧ y ∈ D) → φ)    ⇒   ⊢ ((A ∈ C ∧ B ∈ D) → χ)
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.)
⊢ ℲxA    &   ⊢ ℲyA    &   ⊢ ℲzA    &   ⊢ ℲyB    &   ⊢ ℲzB    &   ⊢ ℲzC    &   ⊢ Ⅎxψ    &   ⊢ Ⅎyχ    &   ⊢ Ⅎzθ    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (z = C → (χ ↔ θ))    &   ⊢ ((x ∈ R ∧ y ∈ S ∧ z ∈ T) → φ)    ⇒   ⊢ ((A ∈ R ∧ B ∈ S ∧ C ∈ T) → θ)
Theorem	vtocl3ga 2925*	Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 20-Aug-1995.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ (z = C → (χ ↔ θ))    &   ⊢ ((x ∈ D ∧ y ∈ R ∧ z ∈ S) → φ)    ⇒   ⊢ ((A ∈ D ∧ B ∈ R ∧ C ∈ S) → θ)
Theorem	vtocleg 2926*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Jan-2004.)
⊢ (x = A → φ)    ⇒   ⊢ (A ∈ V → φ)
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 ∈ B ∧ Ⅎxφ ∧ ∀x(x = A → φ)) → φ)
Theorem	vtoclef 2928*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 18-Aug-1993.)
⊢ Ⅎxφ    &   ⊢ A ∈ V    &   ⊢ (x = A → φ)    ⇒   ⊢ φ
Theorem	vtocle 2929*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 9-Sep-1993.)
⊢ A ∈ V    &   ⊢ (x = A → φ)    ⇒   ⊢ φ
Theorem	vtoclri 2930*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Nov-1994.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ ∀x ∈ B φ    ⇒   ⊢ (A ∈ B → ψ)
Theorem	spcimgft 2931	A closed version of spcimgf 2933. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎxψ    &   ⊢ ℲxA    ⇒   ⊢ (∀x(x = A → (φ → ψ)) → (A ∈ B → (∀xφ → ψ)))
Theorem	spcgft 2932	A closed version of spcgf 2935. (Contributed by Andrew Salmon, 6-Jun-2011.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎxψ    &   ⊢ ℲxA    ⇒   ⊢ (∀x(x = A → (φ ↔ ψ)) → (A ∈ B → (∀xφ → ψ)))
Theorem	spcimgf 2933	Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (φ → ψ))    ⇒   ⊢ (A ∈ V → (∀xφ → ψ))
Theorem	spcimegf 2934	Existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (ψ → φ))    ⇒   ⊢ (A ∈ V → (ψ → ∃xφ))
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.)
⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ V → (∀xφ → ψ))
Theorem	spcegf 2936	Existential specialization, using implicit substitution. (Contributed by NM, 2-Feb-1997.)
⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ V → (ψ → ∃xφ))
Theorem	spcimdv 2937*	Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (φ → A ∈ B)    &   ⊢ ((φ ∧ x = A) → (ψ → χ))    ⇒   ⊢ (φ → (∀xψ → χ))
Theorem	spcdv 2938*	Rule of specialization, using implicit substitution. Analogous to rspcdv 2959. (Contributed by David Moews, 1-May-2017.)
⊢ (φ → A ∈ B)    &   ⊢ ((φ ∧ x = A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀xψ → χ))
Theorem	spcimedv 2939*	Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (φ → A ∈ B)    &   ⊢ ((φ ∧ x = A) → (χ → ψ))    ⇒   ⊢ (φ → (χ → ∃xψ))
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 → (φ ↔ ψ))    ⇒   ⊢ (A ∈ V → (∀xφ → ψ))
Theorem	spcegv 2941*	Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ V → (ψ → ∃xφ))
Theorem	spc2egv 2942*	Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by NM, 3-Aug-1995.)
⊢ ((x = A ∧ y = B) → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ V ∧ B ∈ W) → (ψ → ∃x∃yφ))
Theorem	spc2gv 2943*	Specialization with 2 quantifiers, using implicit substitution. (Contributed by NM, 27-Apr-2004.)
⊢ ((x = A ∧ y = B) → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ V ∧ B ∈ W) → (∀x∀yφ → ψ))
Theorem	spc3egv 2944*	Existential specialization with 3 quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.)
⊢ ((x = A ∧ y = B ∧ z = C) → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) → (ψ → ∃x∃y∃zφ))
Theorem	spc3gv 2945*	Specialization with 3 quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.)
⊢ ((x = A ∧ y = B ∧ z = C) → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ V ∧ B ∈ W ∧ C ∈ X) → (∀x∀y∀zφ → ψ))
Theorem	spcv 2946*	Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.)
⊢ A ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (∀xφ → ψ)
Theorem	spcev 2947*	Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
⊢ A ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (ψ → ∃xφ)
Theorem	spc2ev 2948*	Existential specialization, using implicit substitution. (Contributed by NM, 3-Aug-1995.)
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ ((x = A ∧ y = B) → (φ ↔ ψ))    ⇒   ⊢ (ψ → ∃x∃yφ)
Theorem	rspct 2949*	A closed version of rspc 2950. (Contributed by Andrew Salmon, 6-Jun-2011.)
⊢ Ⅎxψ    ⇒   ⊢ (∀x(x = A → (φ ↔ ψ)) → (A ∈ B → (∀x ∈ B φ → ψ)))
Theorem	rspc 2950*	Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
⊢ Ⅎxψ    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ B → (∀x ∈ B φ → ψ))
Theorem	rspce 2951*	Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro, 11-Oct-2016.)
⊢ Ⅎxψ    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ B ∧ ψ) → ∃x ∈ B φ)
Theorem	rspcv 2952*	Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ B → (∀x ∈ B φ → ψ))
Theorem	rspccv 2953*	Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (∀x ∈ B φ → (A ∈ B → ψ))
Theorem	rspcva 2954*	Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ B ∧ ∀x ∈ B φ) → ψ)
Theorem	rspccva 2955*	Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ ((∀x ∈ B φ ∧ A ∈ B) → ψ)
Theorem	rspcev 2956*	Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ B ∧ ψ) → ∃x ∈ B φ)
Theorem	rspcimdv 2957*	Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (φ → A ∈ B)    &   ⊢ ((φ ∧ x = A) → (ψ → χ))    ⇒   ⊢ (φ → (∀x ∈ B ψ → χ))
Theorem	rspcimedv 2958*	Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (φ → A ∈ B)    &   ⊢ ((φ ∧ x = A) → (χ → ψ))    ⇒   ⊢ (φ → (χ → ∃x ∈ B ψ))
Theorem	rspcdv 2959*	Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ (φ → A ∈ B)    &   ⊢ ((φ ∧ x = A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x ∈ B ψ → χ))
Theorem	rspcedv 2960*	Restricted existential specialization, using implicit substitution. (Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ (φ → A ∈ B)    &   ⊢ ((φ ∧ x = A) → (ψ ↔ χ))    ⇒   ⊢ (φ → (χ → ∃x ∈ B ψ))
Theorem	rspc2 2961*	2-variable restricted specialization, using implicit substitution. (Contributed by NM, 9-Nov-2012.)
⊢ Ⅎxχ    &   ⊢ Ⅎyψ    &   ⊢ (x = A → (φ ↔ χ))    &   ⊢ (y = B → (χ ↔ ψ))    ⇒   ⊢ ((A ∈ C ∧ B ∈ D) → (∀x ∈ C ∀y ∈ D φ → ψ))
Theorem	rspc2v 2962*	2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.)
⊢ (x = A → (φ ↔ χ))    &   ⊢ (y = B → (χ ↔ ψ))    ⇒   ⊢ ((A ∈ C ∧ B ∈ D) → (∀x ∈ C ∀y ∈ D φ → ψ))
Theorem	rspc2va 2963*	2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.)
⊢ (x = A → (φ ↔ χ))    &   ⊢ (y = B → (χ ↔ ψ))    ⇒   ⊢ (((A ∈ C ∧ B ∈ D) ∧ ∀x ∈ C ∀y ∈ D φ) → ψ)
Theorem	rspc2ev 2964*	2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)
⊢ (x = A → (φ ↔ χ))    &   ⊢ (y = B → (χ ↔ ψ))    ⇒   ⊢ ((A ∈ C ∧ B ∈ D ∧ ψ) → ∃x ∈ C ∃y ∈ D φ)
Theorem	rspc3v 2965*	3-variable restricted specialization, using implicit substitution. (Contributed by NM, 10-May-2005.)
⊢ (x = A → (φ ↔ χ))    &   ⊢ (y = B → (χ ↔ θ))    &   ⊢ (z = C → (θ ↔ ψ))    ⇒   ⊢ ((A ∈ R ∧ B ∈ S ∧ C ∈ T) → (∀x ∈ R ∀y ∈ S ∀z ∈ T φ → ψ))
Theorem	rspc3ev 2966*	3-variable restricted existentional specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012.)
⊢ (x = A → (φ ↔ χ))    &   ⊢ (y = B → (χ ↔ θ))    &   ⊢ (z = C → (θ ↔ ψ))    ⇒   ⊢ (((A ∈ R ∧ B ∈ S ∧ C ∈ T) ∧ ψ) → ∃x ∈ R ∃y ∈ S ∃z ∈ T φ)
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 ∈ V    ⇒   ⊢ (A = B ↔ ∃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.)
⊢ ℲxA    &   ⊢ ℲxB    &   ⊢ A ∈ V    ⇒   ⊢ (A = B ↔ ∃x(x = A ∧ x = B))
Theorem	alexeq 2969*	Two ways to express substitution of A for x in φ. (Contributed by NM, 2-Mar-1995.)
⊢ A ∈ V    ⇒   ⊢ (∀x(x = A → φ) ↔ ∃x(x = A ∧ φ))
Theorem	ceqex 2970*	Equality implies equivalence with substitution. (Contributed by NM, 2-Mar-1995.)
⊢ (x = A → (φ ↔ ∃x(x = A ∧ φ)))
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.)
⊢ Ⅎxψ    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ V → (∃x(x = A ∧ φ) ↔ ψ))
Theorem	ceqsexgv 2972*	Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 29-Dec-1996.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ V → (∃x(x = A ∧ φ) ↔ ψ))
Theorem	ceqsrexv 2973*	Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ B → (∃x ∈ B (x = A ∧ φ) ↔ ψ))
Theorem	ceqsrexbv 2974*	Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ B (x = A ∧ φ) ↔ (A ∈ B ∧ ψ))
Theorem	ceqsrex2v 2975*	Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 29-Oct-2005.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    ⇒   ⊢ ((A ∈ C ∧ B ∈ D) → (∃x ∈ C ∃y ∈ D ((x = A ∧ y = B) ∧ φ) ↔ χ))
Theorem	clel2 2976*	An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.)
⊢ A ∈ V    ⇒   ⊢ (A ∈ B ↔ ∀x(x = A → x ∈ B))
Theorem	clel3g 2977*	An alternate definition of class membership when the class is a set. (Contributed by NM, 13-Aug-2005.)
⊢ (B ∈ V → (A ∈ B ↔ ∃x(x = B ∧ A ∈ x)))
Theorem	clel3 2978*	An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.)
⊢ B ∈ V    ⇒   ⊢ (A ∈ B ↔ ∃x(x = B ∧ A ∈ x))
Theorem	clel4 2979*	An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.)
⊢ B ∈ V    ⇒   ⊢ (A ∈ B ↔ ∀x(x = B → A ∈ 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 ∈ V → (A = B ↔ ∀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.)
⊢ (∀x ∈ A ∀y ∈ A φ ↔ ∀x ∈ A φ)
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.)
⊢ (∀x ∈ A ∀y ∈ A (φ ∧ ψ) ↔ ∀x ∈ A (φ ∧ ∀y ∈ A ψ))
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 ∈ B ∧ ∀x(x = A → (φ ↔ ψ))) → (A ∈ {x ∣ φ} ↔ ψ))
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.)
⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ B → (A ∈ {x ∣ φ} ↔ ψ))
Theorem	elabf 2985*	Membership in a class abstraction, using implicit substitution. (Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎxψ    &   ⊢ A ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ {x ∣ φ} ↔ ψ)
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 ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ {x ∣ φ} ↔ ψ)
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 → (φ ↔ ψ))    ⇒   ⊢ (A ∈ V → (A ∈ {x ∣ φ} ↔ ψ))
Theorem	elab2g 2988*	Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ B = {x ∣ φ}    ⇒   ⊢ (A ∈ V → (A ∈ B ↔ ψ))
Theorem	elab2 2989*	Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
⊢ A ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ B = {x ∣ φ}    ⇒   ⊢ (A ∈ B ↔ ψ)
Theorem	elab4g 2990*	Membership in a class abstraction, using implicit substitution. (Contributed by NM, 17-Oct-2012.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ B = {x ∣ φ}    ⇒   ⊢ (A ∈ B ↔ (A ∈ V ∧ ψ))
Theorem	elab3gf 2991	Membership in a class abstraction, with a weaker antecedent than elabgf 2984. (Contributed by NM, 6-Sep-2011.)
⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ ((ψ → A ∈ B) → (A ∈ {x ∣ φ} ↔ ψ))
Theorem	elab3g 2992*	Membership in a class abstraction, with a weaker antecedent than elabg 2987. (Contributed by NM, 29-Aug-2006.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ ((ψ → A ∈ B) → (A ∈ {x ∣ φ} ↔ ψ))
Theorem	elab3 2993*	Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.)
⊢ (ψ → A ∈ V)    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ {x ∣ φ} ↔ ψ)
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.)
⊢ ℲxA    &   ⊢ ℲxB    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ {x ∈ B ∣ φ} ↔ (A ∈ B ∧ ψ))
Theorem	elrab 2995*	Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ {x ∈ B ∣ φ} ↔ (A ∈ B ∧ ψ))
Theorem	elrab3 2996*	Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006.)
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (A ∈ B → (A ∈ {x ∈ B ∣ φ} ↔ ψ))
Theorem	elrab2 2997*	Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.)
⊢ (x = A → (φ ↔ ψ))    &   ⊢ C = {x ∈ B ∣ φ}    ⇒   ⊢ (A ∈ C ↔ (A ∈ B ∧ ψ))
Theorem	ralab 2998*	Universal quantification over a class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (y = x → (φ ↔ ψ))    ⇒   ⊢ (∀x ∈ {y ∣ φ}χ ↔ ∀x(ψ → χ))
Theorem	ralrab 2999*	Universal quantification over a restricted class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (y = x → (φ ↔ ψ))    ⇒   ⊢ (∀x ∈ {y ∈ A ∣ φ}χ ↔ ∀x ∈ A (ψ → χ))
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 → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ {y ∣ φ}χ ↔ ∃x(ψ ∧ χ))