Theorem List for Intuitionistic Logic Explorer - 2901-3000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | sbc5 2901* |
An equivalence for class substitution. (Contributed by NM,
23-Aug-1993.) (Revised by Mario Carneiro, 12-Oct-2016.)
|
   ![]. ].](_drbrack.gif)
      |
|
Theorem | sbc6g 2902* |
An equivalence for class substitution. (Contributed by NM,
11-Oct-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
|
    ![]. ].](_drbrack.gif)
       |
|
Theorem | sbc6 2903* |
An equivalence for class substitution. (Contributed by NM,
23-Aug-1993.) (Proof shortened by Eric Schmidt, 17-Jan-2007.)
|
   ![]. ].](_drbrack.gif)       |
|
Theorem | sbc7 2904* |
An equivalence for class substitution in the spirit of df-clab 2102. Note
that and don't have to be distinct.
(Contributed by NM,
18-Nov-2008.) (Revised by Mario Carneiro, 13-Oct-2016.)
|
   ![]. ].](_drbrack.gif)
     ![]. ].](_drbrack.gif)    |
|
Theorem | cbvsbc 2905 |
Change bound variables in a wff substitution. (Contributed by Jeff
Hankins, 19-Sep-2009.) (Proof shortened by Andrew Salmon,
8-Jun-2011.)
|
    
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
|
Theorem | cbvsbcv 2906* |
Change the bound variable of a class substitution using implicit
substitution. (Contributed by NM, 30-Sep-2008.) (Revised by Mario
Carneiro, 13-Oct-2016.)
|
       ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
|
Theorem | sbciegft 2907* |
Conversion of implicit substitution to explicit class substitution,
using a bound-variable hypothesis instead of distinct variables.
(Closed theorem version of sbciegf 2908.) (Contributed by NM,
10-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.)
|
              ![]. ].](_drbrack.gif)
   |
|
Theorem | sbciegf 2908* |
Conversion of implicit substitution to explicit class substitution.
(Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro,
13-Oct-2016.)
|
  
       ![]. ].](_drbrack.gif)    |
|
Theorem | sbcieg 2909* |
Conversion of implicit substitution to explicit class substitution.
(Contributed by NM, 10-Nov-2005.)
|
        ![]. ].](_drbrack.gif)    |
|
Theorem | sbcie2g 2910* |
Conversion of implicit substitution to explicit class substitution.
This version of sbcie 2911 avoids a disjointness condition on and
by
substituting twice. (Contributed by Mario Carneiro,
15-Oct-2016.)
|
            ![]. ].](_drbrack.gif)    |
|
Theorem | sbcie 2911* |
Conversion of implicit substitution to explicit class substitution.
(Contributed by NM, 4-Sep-2004.)
|

      ![]. ].](_drbrack.gif)   |
|
Theorem | sbciedf 2912* |
Conversion of implicit substitution to explicit class substitution,
deduction form. (Contributed by NM, 29-Dec-2014.)
|
                  ![]. ].](_drbrack.gif)    |
|
Theorem | sbcied 2913* |
Conversion of implicit substitution to explicit class substitution,
deduction form. (Contributed by NM, 13-Dec-2014.)
|
            ![]. ].](_drbrack.gif)    |
|
Theorem | sbcied2 2914* |
Conversion of implicit substitution to explicit class substitution,
deduction form. (Contributed by NM, 13-Dec-2014.)
|
     
        ![]. ].](_drbrack.gif)    |
|
Theorem | elrabsf 2915 |
Membership in a restricted class abstraction, expressed with explicit
class substitution. (The variation elrabf 2807 has implicit substitution).
The hypothesis specifies that must not be a free variable in
. (Contributed
by NM, 30-Sep-2003.) (Proof shortened by Mario
Carneiro, 13-Oct-2016.)
|
   
    ![]. ].](_drbrack.gif)    |
|
Theorem | eqsbc3 2916* |
Substitution applied to an atomic wff. Set theory version of eqsb3 2218.
(Contributed by Andrew Salmon, 29-Jun-2011.)
|
    ![]. ].](_drbrack.gif)    |
|
Theorem | sbcng 2917 |
Move negation in and out of class substitution. (Contributed by NM,
16-Jan-2004.)
|
      ![]. ].](_drbrack.gif)    |
|
Theorem | sbcimg 2918 |
Distribution of class substitution over implication. (Contributed by
NM, 16-Jan-2004.)
|
    ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
|
Theorem | sbcan 2919 |
Distribution of class substitution over conjunction. (Contributed by
NM, 31-Dec-2016.)
|
   ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)    |
|
Theorem | sbcang 2920 |
Distribution of class substitution over conjunction. (Contributed by
NM, 21-May-2004.)
|
    ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)     |
|
Theorem | sbcor 2921 |
Distribution of class substitution over disjunction. (Contributed by
NM, 31-Dec-2016.)
|
   ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
|
Theorem | sbcorg 2922 |
Distribution of class substitution over disjunction. (Contributed by
NM, 21-May-2004.)
|
    ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
|
Theorem | sbcbig 2923 |
Distribution of class substitution over biconditional. (Contributed by
Raph Levien, 10-Apr-2004.)
|
    ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
|
Theorem | sbcn1 2924 |
Move negation in and out of class substitution. One direction of sbcng 2917
that holds for proper classes. (Contributed by NM, 17-Aug-2018.)
|
   
 ![]. ].](_drbrack.gif)   |
|
Theorem | sbcim1 2925 |
Distribution of class substitution over implication. One direction of
sbcimg 2918 that holds for proper classes. (Contributed
by NM,
17-Aug-2018.)
|
   ![]. ].](_drbrack.gif)  
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
|
Theorem | sbcbi1 2926 |
Distribution of class substitution over biconditional. One direction of
sbcbig 2923 that holds for proper classes. (Contributed
by NM,
17-Aug-2018.)
|
   ![]. ].](_drbrack.gif)    
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
|
Theorem | sbcbi2 2927 |
Substituting into equivalent wff's gives equivalent results. (Contributed
by Giovanni Mascellani, 9-Apr-2018.)
|
      
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
|
Theorem | sbcal 2928* |
Move universal quantifier in and out of class substitution.
(Contributed by NM, 31-Dec-2016.)
|
   ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   |
|
Theorem | sbcalg 2929* |
Move universal quantifier in and out of class substitution.
(Contributed by NM, 16-Jan-2004.)
|
    ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)    |
|
Theorem | sbcex2 2930* |
Move existential quantifier in and out of class substitution.
(Contributed by NM, 21-May-2004.)
|
   ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   |
|
Theorem | sbcexg 2931* |
Move existential quantifier in and out of class substitution.
(Contributed by NM, 21-May-2004.)
|
    ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)    |
|
Theorem | sbceqal 2932* |
A variation of extensionality for classes. (Contributed by Andrew
Salmon, 28-Jun-2011.)
|
     
   |
|
Theorem | sbeqalb 2933* |
Theorem *14.121 in [WhiteheadRussell]
p. 185. (Contributed by Andrew
Salmon, 28-Jun-2011.) (Proof shortened by Wolf Lammen, 9-May-2013.)
|
     
     
   |
|
Theorem | sbcbid 2934 |
Formula-building deduction for class substitution. (Contributed by NM,
29-Dec-2014.)
|
          ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
|
Theorem | sbcbidv 2935* |
Formula-building deduction for class substitution. (Contributed by NM,
29-Dec-2014.)
|
        ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
|
Theorem | sbcbii 2936 |
Formula-building inference for class substitution. (Contributed by NM,
11-Nov-2005.)
|
     ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)   |
|
Theorem | eqsbc3r 2937* |
eqsbc3 2916 with setvar variable on right side of equals
sign.
(Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by JJ,
7-Jul-2021.)
|
    ![]. ].](_drbrack.gif)
   |
|
Theorem | sbc3an 2938 |
Distribution of class substitution over triple conjunction. (Contributed
by NM, 14-Dec-2006.) (Revised by NM, 17-Aug-2018.)
|
   ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
|
Theorem | sbcel1v 2939* |
Class substitution into a membership relation. (Contributed by NM,
17-Aug-2018.)
|
   ![]. ].](_drbrack.gif)   |
|
Theorem | sbcel2gv 2940* |
Class substitution into a membership relation. (Contributed by NM,
17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
    ![]. ].](_drbrack.gif)    |
|
Theorem | sbcel21v 2941* |
Class substitution into a membership relation. One direction of
sbcel2gv 2940 that holds for proper classes. (Contributed
by NM,
17-Aug-2018.)
|
   ![]. ].](_drbrack.gif)   |
|
Theorem | sbcimdv 2942* |
Substitution analogue of Theorem 19.20 of [Margaris] p. 90 (alim 1416).
(Contributed by NM, 11-Nov-2005.) (Revised by NM, 17-Aug-2018.) (Proof
shortened by JJ, 7-Jul-2021.)
|
        ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
|
Theorem | sbctt 2943 |
Substitution for a variable not free in a wff does not affect it.
(Contributed by Mario Carneiro, 14-Oct-2016.)
|
        ![]. ].](_drbrack.gif)    |
|
Theorem | sbcgf 2944 |
Substitution for a variable not free in a wff does not affect it.
(Contributed by NM, 11-Oct-2004.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
      ![]. ].](_drbrack.gif)
   |
|
Theorem | sbc19.21g 2945 |
Substitution for a variable not free in antecedent affects only the
consequent. (Contributed by NM, 11-Oct-2004.)
|
      ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)     |
|
Theorem | sbcg 2946* |
Substitution for a variable not occurring in a wff does not affect it.
Distinct variable form of sbcgf 2944. (Contributed by Alan Sare,
10-Nov-2012.)
|
    ![]. ].](_drbrack.gif)
   |
|
Theorem | sbc2iegf 2947* |
Conversion of implicit substitution to explicit class substitution.
(Contributed by Mario Carneiro, 19-Dec-2013.)
|
               
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
|
Theorem | sbc2ie 2948* |
Conversion of implicit substitution to explicit class substitution.
(Contributed by NM, 16-Dec-2008.) (Revised by Mario Carneiro,
19-Dec-2013.)
|
         ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
|
Theorem | sbc2iedv 2949* |
Conversion of implicit substitution to explicit class substitution.
(Contributed by NM, 16-Dec-2008.) (Proof shortened by Mario Carneiro,
18-Oct-2016.)
|
  
     
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
|
Theorem | sbc3ie 2950* |
Conversion of implicit substitution to explicit class substitution.
(Contributed by Mario Carneiro, 19-Jun-2014.) (Revised by Mario
Carneiro, 29-Dec-2014.)
|
 
       ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
|
Theorem | sbccomlem 2951* |
Lemma for sbccom 2952. (Contributed by NM, 14-Nov-2005.) (Revised
by
Mario Carneiro, 18-Oct-2016.)
|
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
|
Theorem | sbccom 2952* |
Commutative law for double class substitution. (Contributed by NM,
15-Nov-2005.) (Proof shortened by Mario Carneiro, 18-Oct-2016.)
|
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
|
Theorem | sbcralt 2953* |
Interchange class substitution and restricted quantifier. (Contributed
by NM, 1-Mar-2008.) (Revised by David Abernethy, 22-Feb-2010.)
|
        ![]. ].](_drbrack.gif) 
   ![]. ].](_drbrack.gif)    |
|
Theorem | sbcrext 2954* |
Interchange class substitution and restricted existential quantifier.
(Contributed by NM, 1-Mar-2008.) (Proof shortened by Mario Carneiro,
13-Oct-2016.)
|
      ![]. ].](_drbrack.gif)     ![]. ].](_drbrack.gif)    |
|
Theorem | sbcralg 2955* |
Interchange class substitution and restricted quantifier. (Contributed
by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
    ![]. ].](_drbrack.gif) 
   ![]. ].](_drbrack.gif)    |
|
Theorem | sbcrex 2956* |
Interchange class substitution and restricted existential quantifier.
(Contributed by NM, 15-Nov-2005.) (Revised by NM, 18-Aug-2018.)
|
   ![]. ].](_drbrack.gif) 
   ![]. ].](_drbrack.gif)   |
|
Theorem | sbcreug 2957* |
Interchange class substitution and restricted unique existential
quantifier. (Contributed by NM, 24-Feb-2013.)
|
    ![]. ].](_drbrack.gif) 
   ![]. ].](_drbrack.gif)    |
|
Theorem | sbcabel 2958* |
Interchange class substitution and class abstraction. (Contributed by
NM, 5-Nov-2005.)
|
      ![]. ].](_drbrack.gif)  
   ![]. ].](_drbrack.gif)     |
|
Theorem | rspsbc 2959* |
Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. This
provides an axiom for a predicate calculus for a restricted domain.
This theorem generalizes the unrestricted stdpc4 1731 and spsbc 2889. See
also rspsbca 2960 and rspcsbela . (Contributed by NM,
17-Nov-2006.)
(Proof shortened by Mario Carneiro, 13-Oct-2016.)
|
  
  ![]. ].](_drbrack.gif)    |
|
Theorem | rspsbca 2960* |
Restricted quantifier version of Axiom 4 of [Mendelson] p. 69.
(Contributed by NM, 14-Dec-2005.)
|
      ![]. ].](_drbrack.gif)   |
|
Theorem | rspesbca 2961* |
Existence form of rspsbca 2960. (Contributed by NM, 29-Feb-2008.) (Proof
shortened by Mario Carneiro, 13-Oct-2016.)
|
    ![]. ].](_drbrack.gif)     |
|
Theorem | spesbc 2962 |
Existence form of spsbc 2889. (Contributed by Mario Carneiro,
18-Nov-2016.)
|
   ![]. ].](_drbrack.gif)
    |
|
Theorem | spesbcd 2963 |
form of spsbc 2889. (Contributed by Mario Carneiro,
9-Feb-2017.)
|
   ![]. ].](_drbrack.gif)       |
|
Theorem | sbcth2 2964* |
A substitution into a theorem. (Contributed by NM, 1-Mar-2008.) (Proof
shortened by Mario Carneiro, 13-Oct-2016.)
|
     ![]. ].](_drbrack.gif)   |
|
Theorem | ra5 2965 |
Restricted quantifier version of Axiom 5 of [Mendelson] p. 69. This is
an axiom of a predicate calculus for a restricted domain. Compare the
unrestricted stdpc5 1546. (Contributed by NM, 16-Jan-2004.)
|
     
     |
|
Theorem | rmo2ilem 2966* |
Condition implying restricted at-most-one quantifier. (Contributed by
Jim Kingdon, 14-Jul-2018.)
|
     
 
   |
|
Theorem | rmo2i 2967* |
Condition implying restricted at-most-one quantifier. (Contributed by
NM, 17-Jun-2017.)
|
       
  |
|
Theorem | rmo3 2968* |
Restricted at-most-one quantifier using explicit substitution.
(Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
|
   
    
 ![] ]](rbrack.gif) 
   |
|
Theorem | rmob 2969* |
Consequence of "at most one", using implicit substitution.
(Contributed
by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.)
|
    
         
     |
|
Theorem | rmoi 2970* |
Consequence of "at most one", using implicit substitution.
(Contributed
by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
|
    
        
    |
|
2.1.10 Proper substitution of classes for sets
into classes
|
|
Syntax | csb 2971 |
Extend class notation to include the proper substitution of a class for a
set into another class.
|
  ![]_ ]_](_urbrack.gif)  |
|
Definition | df-csb 2972* |
Define the proper substitution of a class for a set into another class.
The underlined brackets distinguish it from the substitution into a wff,
wsbc 2878, to prevent ambiguity. Theorem sbcel1g 2988 shows an example of
how ambiguity could arise if we didn't use distinguished brackets.
Theorem sbccsbg 2997 recreates substitution into a wff from this
definition. (Contributed by NM, 10-Nov-2005.)
|

 ![]_ ]_](_urbrack.gif)    ![]. ].](_drbrack.gif)   |
|
Theorem | csb2 2973* |
Alternate expression for the proper substitution into a class, without
referencing substitution into a wff. Note that can be free in
but cannot
occur in .
(Contributed by NM, 2-Dec-2013.)
|

 ![]_ ]_](_urbrack.gif)        |
|
Theorem | csbeq1 2974 |
Analog of dfsbcq 2880 for proper substitution into a class.
(Contributed
by NM, 10-Nov-2005.)
|
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
|
Theorem | cbvcsb 2975 |
Change bound variables in a class substitution. Interestingly, this
does not require any bound variable conditions on . (Contributed
by Jeff Hankins, 13-Sep-2009.) (Revised by Mario Carneiro,
11-Dec-2016.)
|
    
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
|
Theorem | cbvcsbv 2976* |
Change the bound variable of a proper substitution into a class using
implicit substitution. (Contributed by NM, 30-Sep-2008.) (Revised by
Mario Carneiro, 13-Oct-2016.)
|
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)  |
|
Theorem | csbeq1d 2977 |
Equality deduction for proper substitution into a class. (Contributed
by NM, 3-Dec-2005.)
|
     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
|
Theorem | csbid 2978 |
Analog of sbid 1730 for proper substitution into a class.
(Contributed by
NM, 10-Nov-2005.)
|

 ![]_ ]_](_urbrack.gif)  |
|
Theorem | csbeq1a 2979 |
Equality theorem for proper substitution into a class. (Contributed by
NM, 10-Nov-2005.)
|
   ![]_ ]_](_urbrack.gif)   |
|
Theorem | csbco 2980* |
Composition law for chained substitutions into a class. (Contributed by
NM, 10-Nov-2005.)
|

 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
|
Theorem | csbtt 2981 |
Substitution doesn't affect a constant (in which is not
free). (Contributed by Mario Carneiro, 14-Oct-2016.)
|
       ![]_ ]_](_urbrack.gif)   |
|
Theorem | csbconstgf 2982 |
Substitution doesn't affect a constant (in which is not
free). (Contributed by NM, 10-Nov-2005.)
|
     ![]_ ]_](_urbrack.gif)   |
|
Theorem | csbconstg 2983* |
Substitution doesn't affect a constant (in which is not
free). csbconstgf 2982 with distinct variable requirement.
(Contributed by
Alan Sare, 22-Jul-2012.)
|
   ![]_ ]_](_urbrack.gif)   |
|
Theorem | sbcel12g 2984 |
Distribute proper substitution through a membership relation.
(Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
    ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
|
Theorem | sbceqg 2985 |
Distribute proper substitution through an equality relation.
(Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
    ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
|
Theorem | sbcnel12g 2986 |
Distribute proper substitution through negated membership. (Contributed
by Andrew Salmon, 18-Jun-2011.)
|
    ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
|
Theorem | sbcne12g 2987 |
Distribute proper substitution through an inequality. (Contributed by
Andrew Salmon, 18-Jun-2011.)
|
    ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
|
Theorem | sbcel1g 2988* |
Move proper substitution in and out of a membership relation. Note that
the scope of   is the wff , whereas the scope
of   is the class . (Contributed by NM,
10-Nov-2005.)
|
    ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)
   |
|
Theorem | sbceq1g 2989* |
Move proper substitution to first argument of an equality. (Contributed
by NM, 30-Nov-2005.)
|
    ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)
   |
|
Theorem | sbcel2g 2990* |
Move proper substitution in and out of a membership relation.
(Contributed by NM, 14-Nov-2005.)
|
    ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)    |
|
Theorem | sbceq2g 2991* |
Move proper substitution to second argument of an equality.
(Contributed by NM, 30-Nov-2005.)
|
    ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)    |
|
Theorem | csbcomg 2992* |
Commutative law for double substitution into a class. (Contributed by
NM, 14-Nov-2005.)
|
     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
|
Theorem | csbeq2d 2993 |
Formula-building deduction for class substitution. (Contributed by NM,
22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
|
Theorem | csbeq2dv 2994* |
Formula-building deduction for class substitution. (Contributed by NM,
10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
|
Theorem | csbeq2i 2995 |
Formula-building inference for class substitution. (Contributed by NM,
10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
|
Theorem | csbvarg 2996 |
The proper substitution of a class for setvar variable results in the
class (if the class exists). (Contributed by NM, 10-Nov-2005.)
|
   ![]_ ]_](_urbrack.gif)   |
|
Theorem | sbccsbg 2997* |
Substitution into a wff expressed in terms of substitution into a class.
(Contributed by NM, 15-Aug-2007.)
|
    ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
|
Theorem | sbccsb2g 2998 |
Substitution into a wff expressed in using substitution into a class.
(Contributed by NM, 27-Nov-2005.)
|
    ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
|
Theorem | nfcsb1d 2999 |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12-Oct-2016.)
|
         ![]_ ]_](_urbrack.gif)   |
|
Theorem | nfcsb1 3000 |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12-Oct-2016.)
|
      ![]_ ]_](_urbrack.gif)  |