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.)
|
|
|
Theorem | gencbvex2 2902* |
Restatement of gencbvex 2901 with weaker hypotheses. (Contributed by
Jeffrey Hankins, 6-Dec-2006.)
|
|
|
Theorem | gencbval 2903* |
Change of bound variable using implicit substitution. (Contributed by
NM, 17-May-1996.)
|
|
|
Theorem | sbhypf 2904* |
Introduce an explicit substitution into an implicit substitution
hypothesis. See also csbhypf 3171. (Contributed by Raph Levien,
10-Apr-2004.)
|
|
|
Theorem | vtoclgft 2905 |
Closed theorem form of vtoclgf 2913. (Contributed by NM, 17-Feb-2013.)
(Revised by Mario Carneiro, 12-Oct-2016.)
|
|
|
Theorem | vtocldf 2906 |
Implicit substitution of a class for a setvar variable. (Contributed
by Mario Carneiro, 15-Oct-2016.)
|
|
|
Theorem | vtocld 2907* |
Implicit substitution of a class for a setvar variable. (Contributed by
Mario Carneiro, 15-Oct-2016.)
|
|
|
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.)
|
|
|
Theorem | vtocl 2909* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 30-Aug-1993.)
|
|
|
Theorem | vtocl2 2910* |
Implicit substitution of classes for setvar variables. (Contributed by
NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|
|
|
Theorem | vtocl3 2911* |
Implicit substitution of classes for setvar variables. (Contributed by
NM, 3-Jun-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|
|
|
Theorem | vtoclb 2912* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 23-Dec-1993.)
|
|
|
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.)
|
|
|
Theorem | vtoclg 2914* |
Implicit substitution of a class expression for a setvar variable.
(Contributed by NM, 17-Apr-1995.)
|
|
|
Theorem | vtoclbg 2915* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 29-Apr-1994.)
|
|
|
Theorem | vtocl2gf 2916 |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 25-Apr-1995.)
|
|
|
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.)
|
|
|
Theorem | vtocl2g 2918* |
Implicit substitution of 2 classes for 2 setvar variables. (Contributed
by NM, 25-Apr-1995.)
|
|
|
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.)
|
|
|
Theorem | vtoclga 2920* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 20-Aug-1995.)
|
|
|
Theorem | vtocl2gaf 2921* |
Implicit substitution of 2 classes for 2 setvar variables. (Contributed
by NM, 10-Aug-2013.)
|
|
|
Theorem | vtocl2ga 2922* |
Implicit substitution of 2 classes for 2 setvar variables. (Contributed
by NM, 20-Aug-1995.)
|
|
|
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.)
|
|
|
Theorem | vtocl3ga 2924* |
Implicit substitution of 3 classes for 3 setvar variables. (Contributed
by NM, 20-Aug-1995.)
|
|
|
Theorem | vtocleg 2925* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 10-Jan-2004.)
|
|
|
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.)
|
|
|
Theorem | vtoclef 2927* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 18-Aug-1993.)
|
|
|
Theorem | vtocle 2928* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 9-Sep-1993.)
|
|
|
Theorem | vtoclri 2929* |
Implicit substitution of a class for a setvar variable. (Contributed by
NM, 21-Nov-1994.)
|
|
|
Theorem | spcimgft 2930 |
A closed version of spcimgf 2932. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
|
|
Theorem | spcgft 2931 |
A closed version of spcgf 2934. (Contributed by Andrew Salmon,
6-Jun-2011.) (Revised by Mario Carneiro, 4-Jan-2017.)
|
|
|
Theorem | spcimgf 2932 |
Rule of specialization, using implicit substitution. Compare Theorem
7.3 of [Quine] p. 44. (Contributed by
Mario Carneiro, 4-Jan-2017.)
|
|
|
Theorem | spcimegf 2933 |
Existential specialization, using implicit substitution. (Contributed
by Mario Carneiro, 4-Jan-2017.)
|
|
|
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.)
|
|
|
Theorem | spcegf 2935 |
Existential specialization, using implicit substitution. (Contributed
by NM, 2-Feb-1997.)
|
|
|
Theorem | spcimdv 2936* |
Restricted specialization, using implicit substitution. (Contributed
by Mario Carneiro, 4-Jan-2017.)
|
|
|
Theorem | spcdv 2937* |
Rule of specialization, using implicit substitution. Analogous to
rspcdv 2958. (Contributed by David Moews, 1-May-2017.)
|
|
|
Theorem | spcimedv 2938* |
Restricted existential specialization, using implicit substitution.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
|
|
Theorem | spcgv 2939* |
Rule of specialization, using implicit substitution. Compare Theorem
7.3 of [Quine] p. 44. (Contributed by NM,
22-Jun-1994.)
|
|
|
Theorem | spcegv 2940* |
Existential specialization, using implicit substitution. (Contributed
by NM, 14-Aug-1994.)
|
|
|
Theorem | spc2egv 2941* |
Existential specialization with 2 quantifiers, using implicit
substitution. (Contributed by NM, 3-Aug-1995.)
|
|
|
Theorem | spc2gv 2942* |
Specialization with 2 quantifiers, using implicit substitution.
(Contributed by NM, 27-Apr-2004.)
|
|
|
Theorem | spc3egv 2943* |
Existential specialization with 3 quantifiers, using implicit
substitution. (Contributed by NM, 12-May-2008.)
|
|
|
Theorem | spc3gv 2944* |
Specialization with 3 quantifiers, using implicit substitution.
(Contributed by NM, 12-May-2008.)
|
|
|
Theorem | spcv 2945* |
Rule of specialization, using implicit substitution. (Contributed by
NM, 22-Jun-1994.)
|
|
|
Theorem | spcev 2946* |
Existential specialization, using implicit substitution. (Contributed
by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
|
|
|
Theorem | spc2ev 2947* |
Existential specialization, using implicit substitution. (Contributed
by NM, 3-Aug-1995.)
|
|
|
Theorem | rspct 2948* |
A closed version of rspc 2949. (Contributed by Andrew Salmon,
6-Jun-2011.)
|
|
|
Theorem | rspc 2949* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
|
|
|
Theorem | rspce 2950* |
Restricted existential specialization, using implicit substitution.
(Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro,
11-Oct-2016.)
|
|
|
Theorem | rspcv 2951* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 26-May-1998.)
|
|
|
Theorem | rspccv 2952* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 2-Feb-2006.)
|
|
|
Theorem | rspcva 2953* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 13-Sep-2005.)
|
|
|
Theorem | rspccva 2954* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|
|
|
Theorem | rspcev 2955* |
Restricted existential specialization, using implicit substitution.
(Contributed by NM, 26-May-1998.)
|
|
|
Theorem | rspcimdv 2956* |
Restricted specialization, using implicit substitution. (Contributed
by Mario Carneiro, 4-Jan-2017.)
|
|
|
Theorem | rspcimedv 2957* |
Restricted existential specialization, using implicit substitution.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
|
|
Theorem | rspcdv 2958* |
Restricted specialization, using implicit substitution. (Contributed by
NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
|
|
|
Theorem | rspcedv 2959* |
Restricted existential specialization, using implicit substitution.
(Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro,
4-Jan-2017.)
|
|
|
Theorem | rspc2 2960* |
2-variable restricted specialization, using implicit substitution.
(Contributed by NM, 9-Nov-2012.)
|
|
|
Theorem | rspc2v 2961* |
2-variable restricted specialization, using implicit substitution.
(Contributed by NM, 13-Sep-1999.)
|
|
|
Theorem | rspc2va 2962* |
2-variable restricted specialization, using implicit substitution.
(Contributed by NM, 18-Jun-2014.)
|
|
|
Theorem | rspc2ev 2963* |
2-variable restricted existential specialization, using implicit
substitution. (Contributed by NM, 16-Oct-1999.)
|
|
|
Theorem | rspc3v 2964* |
3-variable restricted specialization, using implicit substitution.
(Contributed by NM, 10-May-2005.)
|
|
|
Theorem | rspc3ev 2965* |
3-variable restricted existentional specialization, using implicit
substitution. (Contributed by NM, 25-Jul-2012.)
|
|
|
Theorem | eqvinc 2966* |
A variable introduction law for class equality. (Contributed by NM,
14-Apr-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|
|
|
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.)
|
|
|
Theorem | alexeq 2968* |
Two ways to express substitution of for in .
(Contributed by NM, 2-Mar-1995.)
|
|
|
Theorem | ceqex 2969* |
Equality implies equivalence with substitution. (Contributed by NM,
2-Mar-1995.)
|
|
|
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.)
|
|
|
Theorem | ceqsexgv 2971* |
Elimination of an existential quantifier, using implicit substitution.
(Contributed by NM, 29-Dec-1996.)
|
|
|
Theorem | ceqsrexv 2972* |
Elimination of a restricted existential quantifier, using implicit
substitution. (Contributed by NM, 30-Apr-2004.)
|
|
|
Theorem | ceqsrexbv 2973* |
Elimination of a restricted existential quantifier, using implicit
substitution. (Contributed by Mario Carneiro, 14-Mar-2014.)
|
|
|
Theorem | ceqsrex2v 2974* |
Elimination of a restricted existential quantifier, using implicit
substitution. (Contributed by NM, 29-Oct-2005.)
|
|
|
Theorem | clel2 2975* |
An alternate definition of class membership when the class is a set.
(Contributed by NM, 18-Aug-1993.)
|
|
|
Theorem | clel3g 2976* |
An alternate definition of class membership when the class is a set.
(Contributed by NM, 13-Aug-2005.)
|
|
|
Theorem | clel3 2977* |
An alternate definition of class membership when the class is a set.
(Contributed by NM, 18-Aug-1993.)
|
|
|
Theorem | clel4 2978* |
An alternate definition of class membership when the class is a set.
(Contributed by NM, 18-Aug-1993.)
|
|
|
Theorem | pm13.183 2979* |
Compare theorem *13.183 in [WhiteheadRussell] p. 178. Only is
required to be a set. (Contributed by Andrew Salmon, 3-Jun-2011.)
|
|
|
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.)
|
|
|
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.)
|
|
|
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.)
|
|
|
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.)
|
|
|
Theorem | elabf 2984* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro,
12-Oct-2016.)
|
|
|
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.)
|
|
|
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.)
|
|
|
Theorem | elab2g 2987* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 13-Sep-1995.)
|
|
|
Theorem | elab2 2988* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 13-Sep-1995.)
|
|
|
Theorem | elab4g 2989* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 17-Oct-2012.)
|
|
|
Theorem | elab3gf 2990 |
Membership in a class abstraction, with a weaker antecedent than
elabgf 2983. (Contributed by NM, 6-Sep-2011.)
|
|
|
Theorem | elab3g 2991* |
Membership in a class abstraction, with a weaker antecedent than
elabg 2986. (Contributed by NM, 29-Aug-2006.)
|
|
|
Theorem | elab3 2992* |
Membership in a class abstraction using implicit substitution.
(Contributed by NM, 10-Nov-2000.)
|
|
|
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.)
|
|
|
Theorem | elrab 2994* |
Membership in a restricted class abstraction, using implicit
substitution. (Contributed by NM, 21-May-1999.)
|
|
|
Theorem | elrab3 2995* |
Membership in a restricted class abstraction, using implicit
substitution. (Contributed by NM, 5-Oct-2006.)
|
|
|
Theorem | elrab2 2996* |
Membership in a class abstraction, using implicit substitution.
(Contributed by NM, 2-Nov-2006.)
|
|
|
Theorem | ralab 2997* |
Universal quantification over a class abstraction. (Contributed by Jeff
Madsen, 10-Jun-2010.)
|
|
|
Theorem | ralrab 2998* |
Universal quantification over a restricted class abstraction.
(Contributed by Jeff Madsen, 10-Jun-2010.)
|
|
|
Theorem | rexab 2999* |
Existential quantification over a class abstraction. (Contributed by
Mario Carneiro, 23-Jan-2014.) (Revised by Mario Carneiro,
3-Sep-2015.)
|
|
|
Theorem | rexrab 3000* |
Existential quantification over a class abstraction. (Contributed by
Jeff Madsen, 17-Jun-2011.) (Revised by Mario Carneiro, 3-Sep-2015.)
|
|