Type  Label  Description 
Statement 

Theorem  gencbvex 2901* 
Change of bound variable using implicit substitution. (Contributed by
NM, 17May1996.) (Proof shortened by Andrew Salmon, 8Jun2011.)



Theorem  gencbvex2 2902* 
Restatement of gencbvex 2901 with weaker hypotheses. (Contributed by
Jeffrey Hankins, 6Dec2006.)



Theorem  gencbval 2903* 
Change of bound variable using implicit substitution. (Contributed by
NM, 17May1996.)



Theorem  sbhypf 2904* 
Introduce an explicit substitution into an implicit substitution
hypothesis. See also csbhypf 3171. (Contributed by Raph Levien,
10Apr2004.)



Theorem  vtoclgft 2905 
Closed theorem form of vtoclgf 2913. (Contributed by NM, 17Feb2013.)
(Revised by Mario Carneiro, 12Oct2016.)



Theorem  vtocldf 2906 
Implicit substitution of a class for a setvar variable. (Contributed
by Mario Carneiro, 15Oct2016.)



Theorem  vtocld 2907* 
Implicit substitution of a class for a setvar variable. (Contributed by
Mario Carneiro, 15Oct2016.)



Theorem  vtoclf 2908* 
Implicit substitution of a class for a setvar variable. This is a
generalization of chvar 1986. (Contributed by NM, 30Aug1993.)



Theorem  vtocl 2909* 
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 30Aug1993.)



Theorem  vtocl2 2910* 
Implicit substitution of classes for setvar variables. (Contributed by
NM, 26Jul1995.) (Proof shortened by Andrew Salmon, 8Jun2011.)



Theorem  vtocl3 2911* 
Implicit substitution of classes for setvar variables. (Contributed by
NM, 3Jun1995.) (Proof shortened by Andrew Salmon, 8Jun2011.)



Theorem  vtoclb 2912* 
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 23Dec1993.)



Theorem  vtoclgf 2913 
Implicit substitution of a class for a setvar variable, with
boundvariable hypotheses in place of distinct variable restrictions.
(Contributed by NM, 21Sep2003.) (Proof shortened by Mario Carneiro,
10Oct2016.)



Theorem  vtoclg 2914* 
Implicit substitution of a class expression for a setvar variable.
(Contributed by NM, 17Apr1995.)



Theorem  vtoclbg 2915* 
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 29Apr1994.)



Theorem  vtocl2gf 2916 
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 25Apr1995.)



Theorem  vtocl3gf 2917 
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 10Aug2013.) (Revised by Mario Carneiro, 10Oct2016.)



Theorem  vtocl2g 2918* 
Implicit substitution of 2 classes for 2 setvar variables. (Contributed
by NM, 25Apr1995.)



Theorem  vtoclgaf 2919* 
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 17Feb2006.) (Revised by Mario Carneiro, 10Oct2016.)



Theorem  vtoclga 2920* 
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 20Aug1995.)



Theorem  vtocl2gaf 2921* 
Implicit substitution of 2 classes for 2 setvar variables. (Contributed
by NM, 10Aug2013.)



Theorem  vtocl2ga 2922* 
Implicit substitution of 2 classes for 2 setvar variables. (Contributed
by NM, 20Aug1995.)



Theorem  vtocl3gaf 2923* 
Implicit substitution of 3 classes for 3 setvar variables. (Contributed
by NM, 10Aug2013.) (Revised by Mario Carneiro, 11Oct2016.)



Theorem  vtocl3ga 2924* 
Implicit substitution of 3 classes for 3 setvar variables. (Contributed
by NM, 20Aug1995.)



Theorem  vtocleg 2925* 
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 10Jan2004.)



Theorem  vtoclegft 2926* 
Implicit substitution of a class for a setvar variable. (Closed theorem
version of vtoclef 2927.) (Contributed by NM, 7Nov2005.) (Revised
by
Mario Carneiro, 11Oct2016.)



Theorem  vtoclef 2927* 
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 18Aug1993.)



Theorem  vtocle 2928* 
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 9Sep1993.)



Theorem  vtoclri 2929* 
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 21Nov1994.)



Theorem  spcimgft 2930 
A closed version of spcimgf 2932. (Contributed by Mario Carneiro,
4Jan2017.)



Theorem  spcgft 2931 
A closed version of spcgf 2934. (Contributed by Andrew Salmon,
6Jun2011.) (Revised by Mario Carneiro, 4Jan2017.)



Theorem  spcimgf 2932 
Rule of specialization, using implicit substitution. Compare Theorem
7.3 of [Quine] p. 44. (Contributed by
Mario Carneiro, 4Jan2017.)



Theorem  spcimegf 2933 
Existential specialization, using implicit substitution. (Contributed
by Mario Carneiro, 4Jan2017.)



Theorem  spcgf 2934 
Rule of specialization, using implicit substitution. Compare Theorem
7.3 of [Quine] p. 44. (Contributed by NM,
2Feb1997.) (Revised by
Andrew Salmon, 12Aug2011.)



Theorem  spcegf 2935 
Existential specialization, using implicit substitution. (Contributed
by NM, 2Feb1997.)



Theorem  spcimdv 2936* 
Restricted specialization, using implicit substitution. (Contributed
by Mario Carneiro, 4Jan2017.)



Theorem  spcdv 2937* 
Rule of specialization, using implicit substitution. Analogous to
rspcdv 2958. (Contributed by David Moews, 1May2017.)



Theorem  spcimedv 2938* 
Restricted existential specialization, using implicit substitution.
(Contributed by Mario Carneiro, 4Jan2017.)



Theorem  spcgv 2939* 
Rule of specialization, using implicit substitution. Compare Theorem
7.3 of [Quine] p. 44. (Contributed by NM,
22Jun1994.)



Theorem  spcegv 2940* 
Existential specialization, using implicit substitution. (Contributed
by NM, 14Aug1994.)



Theorem  spc2egv 2941* 
Existential specialization with 2 quantifiers, using implicit
substitution. (Contributed by NM, 3Aug1995.)



Theorem  spc2gv 2942* 
Specialization with 2 quantifiers, using implicit substitution.
(Contributed by NM, 27Apr2004.)



Theorem  spc3egv 2943* 
Existential specialization with 3 quantifiers, using implicit
substitution. (Contributed by NM, 12May2008.)



Theorem  spc3gv 2944* 
Specialization with 3 quantifiers, using implicit substitution.
(Contributed by NM, 12May2008.)



Theorem  spcv 2945* 
Rule of specialization, using implicit substitution. (Contributed by
NM, 22Jun1994.)



Theorem  spcev 2946* 
Existential specialization, using implicit substitution. (Contributed
by NM, 31Dec1993.) (Proof shortened by Eric Schmidt, 22Dec2006.)



Theorem  spc2ev 2947* 
Existential specialization, using implicit substitution. (Contributed
by NM, 3Aug1995.)



Theorem  rspct 2948* 
A closed version of rspc 2949. (Contributed by Andrew Salmon,
6Jun2011.)



Theorem  rspc 2949* 
Restricted specialization, using implicit substitution. (Contributed by
NM, 19Apr2005.) (Revised by Mario Carneiro, 11Oct2016.)



Theorem  rspce 2950* 
Restricted existential specialization, using implicit substitution.
(Contributed by NM, 26May1998.) (Revised by Mario Carneiro,
11Oct2016.)



Theorem  rspcv 2951* 
Restricted specialization, using implicit substitution. (Contributed by
NM, 26May1998.)



Theorem  rspccv 2952* 
Restricted specialization, using implicit substitution. (Contributed by
NM, 2Feb2006.)



Theorem  rspcva 2953* 
Restricted specialization, using implicit substitution. (Contributed by
NM, 13Sep2005.)



Theorem  rspccva 2954* 
Restricted specialization, using implicit substitution. (Contributed by
NM, 26Jul2006.) (Proof shortened by Andrew Salmon, 8Jun2011.)



Theorem  rspcev 2955* 
Restricted existential specialization, using implicit substitution.
(Contributed by NM, 26May1998.)



Theorem  rspcimdv 2956* 
Restricted specialization, using implicit substitution. (Contributed
by Mario Carneiro, 4Jan2017.)



Theorem  rspcimedv 2957* 
Restricted existential specialization, using implicit substitution.
(Contributed by Mario Carneiro, 4Jan2017.)



Theorem  rspcdv 2958* 
Restricted specialization, using implicit substitution. (Contributed by
NM, 17Feb2007.) (Revised by Mario Carneiro, 4Jan2017.)



Theorem  rspcedv 2959* 
Restricted existential specialization, using implicit substitution.
(Contributed by FL, 17Apr2007.) (Revised by Mario Carneiro,
4Jan2017.)



Theorem  rspc2 2960* 
2variable restricted specialization, using implicit substitution.
(Contributed by NM, 9Nov2012.)



Theorem  rspc2v 2961* 
2variable restricted specialization, using implicit substitution.
(Contributed by NM, 13Sep1999.)



Theorem  rspc2va 2962* 
2variable restricted specialization, using implicit substitution.
(Contributed by NM, 18Jun2014.)



Theorem  rspc2ev 2963* 
2variable restricted existential specialization, using implicit
substitution. (Contributed by NM, 16Oct1999.)



Theorem  rspc3v 2964* 
3variable restricted specialization, using implicit substitution.
(Contributed by NM, 10May2005.)



Theorem  rspc3ev 2965* 
3variable restricted existentional specialization, using implicit
substitution. (Contributed by NM, 25Jul2012.)



Theorem  eqvinc 2966* 
A variable introduction law for class equality. (Contributed by NM,
14Apr1995.) (Proof shortened by Andrew Salmon, 8Jun2011.)



Theorem  eqvincf 2967 
A variable introduction law for class equality, using boundvariable
hypotheses instead of distinct variable conditions. (Contributed by NM,
14Sep2003.)



Theorem  alexeq 2968* 
Two ways to express substitution of for in .
(Contributed by NM, 2Mar1995.)



Theorem  ceqex 2969* 
Equality implies equivalence with substitution. (Contributed by NM,
2Mar1995.)



Theorem  ceqsexg 2970* 
A representation of explicit substitution of a class for a variable,
inferred from an implicit substitution hypothesis. (Contributed by NM,
11Oct2004.)



Theorem  ceqsexgv 2971* 
Elimination of an existential quantifier, using implicit substitution.
(Contributed by NM, 29Dec1996.)



Theorem  ceqsrexv 2972* 
Elimination of a restricted existential quantifier, using implicit
substitution. (Contributed by NM, 30Apr2004.)



Theorem  ceqsrexbv 2973* 
Elimination of a restricted existential quantifier, using implicit
substitution. (Contributed by Mario Carneiro, 14Mar2014.)



Theorem  ceqsrex2v 2974* 
Elimination of a restricted existential quantifier, using implicit
substitution. (Contributed by NM, 29Oct2005.)



Theorem  clel2 2975* 
An alternate definition of class membership when the class is a set.
(Contributed by NM, 18Aug1993.)



Theorem  clel3g 2976* 
An alternate definition of class membership when the class is a set.
(Contributed by NM, 13Aug2005.)



Theorem  clel3 2977* 
An alternate definition of class membership when the class is a set.
(Contributed by NM, 18Aug1993.)



Theorem  clel4 2978* 
An alternate definition of class membership when the class is a set.
(Contributed by NM, 18Aug1993.)



Theorem  pm13.183 2979* 
Compare theorem *13.183 in [WhiteheadRussell] p. 178. Only is
required to be a set. (Contributed by Andrew Salmon, 3Jun2011.)



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, 25Oct2012.)



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, 29Oct2012.)



Theorem  elabgt 2982* 
Membership in a class abstraction, using implicit substitution. (Closed
theorem version of elabg 2986.) (Contributed by NM, 7Nov2005.) (Proof
shortened by Andrew Salmon, 8Jun2011.)



Theorem  elabgf 2983 
Membership in a class abstraction, using implicit substitution. Compare
Theorem 6.13 of [Quine] p. 44. This
version has boundvariable
hypotheses in place of distinct variable restrictions. (Contributed by
NM, 21Sep2003.) (Revised by Mario Carneiro, 12Oct2016.)



Theorem  elabf 2984* 
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 1Aug1994.) (Revised by Mario Carneiro,
12Oct2016.)



Theorem  elab 2985* 
Membership in a class abstraction, using implicit substitution. Compare
Theorem 6.13 of [Quine] p. 44.
(Contributed by NM, 1Aug1994.)



Theorem  elabg 2986* 
Membership in a class abstraction, using implicit substitution. Compare
Theorem 6.13 of [Quine] p. 44.
(Contributed by NM, 14Apr1995.)



Theorem  elab2g 2987* 
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 13Sep1995.)



Theorem  elab2 2988* 
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 13Sep1995.)



Theorem  elab4g 2989* 
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 17Oct2012.)



Theorem  elab3gf 2990 
Membership in a class abstraction, with a weaker antecedent than
elabgf 2983. (Contributed by NM, 6Sep2011.)



Theorem  elab3g 2991* 
Membership in a class abstraction, with a weaker antecedent than
elabg 2986. (Contributed by NM, 29Aug2006.)



Theorem  elab3 2992* 
Membership in a class abstraction using implicit substitution.
(Contributed by NM, 10Nov2000.)



Theorem  elrabf 2993 
Membership in a restricted class abstraction, using implicit
substitution. This version has boundvariable hypotheses in place of
distinct variable restrictions. (Contributed by NM, 21Sep2003.)



Theorem  elrab 2994* 
Membership in a restricted class abstraction, using implicit
substitution. (Contributed by NM, 21May1999.)



Theorem  elrab3 2995* 
Membership in a restricted class abstraction, using implicit
substitution. (Contributed by NM, 5Oct2006.)



Theorem  elrab2 2996* 
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 2Nov2006.)



Theorem  ralab 2997* 
Universal quantification over a class abstraction. (Contributed by Jeff
Madsen, 10Jun2010.)



Theorem  ralrab 2998* 
Universal quantification over a restricted class abstraction.
(Contributed by Jeff Madsen, 10Jun2010.)



Theorem  rexab 2999* 
Existential quantification over a class abstraction. (Contributed by
Mario Carneiro, 23Jan2014.) (Revised by Mario Carneiro,
3Sep2015.)



Theorem  rexrab 3000* 
Existential quantification over a class abstraction. (Contributed by
Jeff Madsen, 17Jun2011.) (Revised by Mario Carneiro, 3Sep2015.)

