Type  Label  Description 
Statement 

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



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



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



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



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



Theorem  vtoclgf 2606 
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 2607* 
Implicit substitution of a class expression for a setvar variable.
(Contributed by NM, 17Apr1995.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  spcimegft 2625 
A closed version of spcimegf 2628. (Contributed by Mario Carneiro,
4Jan2017.)



Theorem  spcegft 2626 
A closed version of spcegf 2630. (Contributed by Jim Kingdon,
22Jun2018.)



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



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



Theorem  spcgf 2629 
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 2630 
Existential specialization, using implicit substitution. (Contributed
by NM, 2Feb1997.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  eqvincg 2662* 
A variable introduction law for class equality, deduction version.
(Contributed by Thierry Arnoux, 2Mar2017.)



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  rr19.3v 2676* 
Restricted quantifier version of Theorem 19.3 of [Margaris] p. 89.
(Contributed by NM, 25Oct2012.)



Theorem  rr19.28v 2677* 
Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90.
(Contributed by NM, 29Oct2012.)



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



Theorem  elabgf 2679 
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 2680* 
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 1Aug1994.) (Revised by Mario Carneiro,
12Oct2016.)



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



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



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



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



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



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



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



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



Theorem  elrabi 2689* 
Implication for the membership in a restricted class abstraction.
(Contributed by Alexander van der Vekens, 31Dec2017.)



Theorem  elrabf 2690 
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  elrab3t 2691* 
Membership in a restricted class abstraction, using implicit
substitution. (Closed theorem version of elrab3 2693.) (Contributed by
Thierry Arnoux, 31Aug2017.)



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



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



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



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



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



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



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



Theorem  ralab2 2699* 
Universal quantification over a class abstraction. (Contributed by
Mario Carneiro, 3Sep2015.)



Theorem  ralrab2 2700* 
Universal quantification over a restricted class abstraction.
(Contributed by Mario Carneiro, 3Sep2015.)

