Theorem List for New Foundations Explorer - 3101-3200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | sbcbii 3101 |
Formula-building inference rule for class substitution. (Contributed by
NM, 11-Nov-2005.)
|
     ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
|
Theorem | sbcbiiOLD 3102 |
Formula-building inference rule for class substitution. (Contributed by
NM, 11-Nov-2005.) (New usage is discouraged.)
|
      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
|
Theorem | eqsbc3r 3103* |
eqsbc3 3085 with setvar variable on right side of equals
sign. This proof
was automatically generated from the virtual deduction proof eqsbc3rVD
in set.mm using a translation program. (Contributed by Alan Sare,
24-Oct-2011.)
|
    ![]. ].](_drbrack.gif)
   |
|
Theorem | sbc3ang 3104 |
Distribution of class substitution over triple conjunction.
(Contributed by NM, 14-Dec-2006.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
    ![]. ].](_drbrack.gif)  
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
|
Theorem | sbcel1gv 3105* |
Class substitution into a membership relation. (Contributed by NM,
17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
    ![]. ].](_drbrack.gif)    |
|
Theorem | sbcel2gv 3106* |
Class substitution into a membership relation. (Contributed by NM,
17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
    ![]. ].](_drbrack.gif)    |
|
Theorem | sbcimdv 3107* |
Substitution analog of Theorem 19.20 of [Margaris] p. 90. (Contributed
by NM, 11-Nov-2005.)
|
          ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
|
Theorem | sbctt 3108 |
Substitution for a variable not free in a wff does not affect it.
(Contributed by Mario Carneiro, 14-Oct-2016.)
|
        ![]. ].](_drbrack.gif)    |
|
Theorem | sbcgf 3109 |
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 3110 |
Substitution for a variable not free in antecedent affects only the
consequent. (Contributed by NM, 11-Oct-2004.)
|
      ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)     |
|
Theorem | sbcg 3111* |
Substitution for a variable not occurring in a wff does not affect it.
Distinct variable form of sbcgf 3109. (Contributed by Alan Sare,
10-Nov-2012.)
|
    ![]. ].](_drbrack.gif)
   |
|
Theorem | sbc2iegf 3112* |
Conversion of implicit substitution to explicit class substitution.
(Contributed by Mario Carneiro, 19-Dec-2013.)
|
                 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
|
Theorem | sbc2ie 3113* |
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 3114* |
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 3115* |
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 3116* |
Lemma for sbccom 3117. (Contributed by NM, 14-Nov-2005.) (Revised
by
Mario Carneiro, 18-Oct-2016.)
|
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   |
|
Theorem | sbccom 3117* |
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 3118* |
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 3119* |
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 3120* |
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 | sbcrexg 3121* |
Interchange class substitution and restricted existential quantifier.
(Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon,
29-Jun-2011.)
|
    ![]. ].](_drbrack.gif)     ![]. ].](_drbrack.gif)    |
|
Theorem | sbcreug 3122* |
Interchange class substitution and restricted uniqueness quantifier.
(Contributed by NM, 24-Feb-2013.)
|
    ![]. ].](_drbrack.gif)     ![]. ].](_drbrack.gif)    |
|
Theorem | sbcabel 3123* |
Interchange class substitution and class abstraction. (Contributed by
NM, 5-Nov-2005.)
|
      ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)     |
|
Theorem | rspsbc 3124* |
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 2024 and spsbc 3058. See
also rspsbca 3125 and rspcsbela 3195. (Contributed by NM, 17-Nov-2006.)
(Proof shortened by Mario Carneiro, 13-Oct-2016.)
|
     ![]. ].](_drbrack.gif)    |
|
Theorem | rspsbca 3125* |
Restricted quantifier version of Axiom 4 of [Mendelson] p. 69.
(Contributed by NM, 14-Dec-2005.)
|
      ![]. ].](_drbrack.gif)   |
|
Theorem | rspesbca 3126* |
Existence form of rspsbca 3125. (Contributed by NM, 29-Feb-2008.) (Proof
shortened by Mario Carneiro, 13-Oct-2016.)
|
    ![]. ].](_drbrack.gif)  
  |
|
Theorem | spesbc 3127 |
Existence form of spsbc 3058. (Contributed by Mario Carneiro,
18-Nov-2016.)
|
   ![]. ].](_drbrack.gif)
    |
|
Theorem | spesbcd 3128 |
form of spsbc 3058. (Contributed by Mario Carneiro,
9-Feb-2017.)
|
   ![]. ].](_drbrack.gif)       |
|
Theorem | sbcth2 3129* |
A substitution into a theorem. (Contributed by NM, 1-Mar-2008.) (Proof
shortened by Mario Carneiro, 13-Oct-2016.)
|
     ![]. ].](_drbrack.gif)   |
|
Theorem | ra5 3130 |
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 1798. (Contributed by NM, 16-Jan-2004.)
|
           |
|
Theorem | rmo2 3131* |
Alternate definition of restricted "at most one." Note that
  is
not equivalent to
      (in analogy to reu6 3025); to see
this, let be
the empty set. However, one direction of this
pattern holds; see rmo2i 3132. (Contributed by NM, 17-Jun-2017.)
|
           |
|
Theorem | rmo2i 3132* |
Condition implying restricted "at most one." (Contributed by NM,
17-Jun-2017.)
|
      
   |
|
Theorem | rmo3 3133* |
Restricted "at most one" using explicit substitution. (Contributed
by
NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
|
          ![]](rbrack.gif)     |
|
Theorem | rmob 3134* |
Consequence of "at most one", using implicit substitution.
(Contributed
by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.)
|
          
  
      |
|
Theorem | rmoi 3135* |
Consequence of "at most one", using implicit substitution.
(Contributed
by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.)
|
          
       |
|
2.1.9 Proper substitution of classes for sets
into classes
|
|
Syntax | csb 3136 |
Extend class notation to include the proper substitution of a class for a
set into another class.
|
  ![]_](_urbrack.gif)  |
|
Definition | df-csb 3137* |
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 3046, to prevent ambiguity. Theorem sbcel1g 3155 shows an example of
how ambiguity could arise if we didn't use distinguished brackets.
Theorem sbccsbg 3164 recreates substitution into a wff from this
definition. (Contributed by NM, 10-Nov-2005.)
|
  ![]_](_urbrack.gif)
   ![]. ].](_drbrack.gif)   |
|
Theorem | csb2 3138* |
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 3139 |
Analog of dfsbcq 3048 for proper substitution into a class.
(Contributed
by NM, 10-Nov-2005.)
|
   ![]_](_urbrack.gif)   ![]_](_urbrack.gif)   |
|
Theorem | cbvcsb 3140 |
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 3141* |
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 3142 |
Equality deduction for proper substitution into a class. (Contributed
by NM, 3-Dec-2005.)
|
     ![]_](_urbrack.gif)   ![]_](_urbrack.gif)   |
|
Theorem | csbid 3143 |
Analog of sbid 1922 for proper substitution into a class.
(Contributed by
NM, 10-Nov-2005.)
|

 ![]_](_urbrack.gif)
 |
|
Theorem | csbeq1a 3144 |
Equality theorem for proper substitution into a class. (Contributed by
NM, 10-Nov-2005.)
|
   ![]_](_urbrack.gif)   |
|
Theorem | csbco 3145* |
Composition law for chained substitutions into a class. (Contributed by
NM, 10-Nov-2005.)
|
  ![]_](_urbrack.gif)   ![]_](_urbrack.gif)
  ![]_](_urbrack.gif)  |
|
Theorem | csbexg 3146 |
The existence of proper substitution into a class. (Contributed by NM,
10-Nov-2005.)
|
      ![]_](_urbrack.gif)   |
|
Theorem | csbex 3147 |
The existence of proper substitution into a class. (Contributed by NM,
7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|
  ![]_](_urbrack.gif)  |
|
Theorem | csbtt 3148 |
Substitution doesn't affect a constant (in which is not
free). (Contributed by Mario Carneiro, 14-Oct-2016.)
|
       ![]_](_urbrack.gif)   |
|
Theorem | csbconstgf 3149 |
Substitution doesn't affect a constant (in which is not
free). (Contributed by NM, 10-Nov-2005.)
|
     ![]_](_urbrack.gif)   |
|
Theorem | csbconstg 3150* |
Substitution doesn't affect a constant (in which is not
free). csbconstgf 3149 with distinct variable requirement.
(Contributed by
Alan Sare, 22-Jul-2012.)
|
   ![]_](_urbrack.gif)   |
|
Theorem | sbcel12g 3151 |
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 3152 |
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 3153 |
Distribute proper substitution through negated membership. (Contributed
by Andrew Salmon, 18-Jun-2011.)
|
    ![]. ].](_drbrack.gif)   ![]_](_urbrack.gif)   ![]_](_urbrack.gif)    |
|
Theorem | sbcne12g 3154 |
Distribute proper substitution through an inequality. (Contributed by
Andrew Salmon, 18-Jun-2011.)
|
    ![]. ].](_drbrack.gif)   ![]_](_urbrack.gif)   ![]_](_urbrack.gif)    |
|
Theorem | sbcel1g 3155* |
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 3156* |
Move proper substitution to first argument of an equality. (Contributed
by NM, 30-Nov-2005.)
|
    ![]. ].](_drbrack.gif)   ![]_](_urbrack.gif)
   |
|
Theorem | sbcel2g 3157* |
Move proper substitution in and out of a membership relation.
(Contributed by NM, 14-Nov-2005.)
|
    ![]. ].](_drbrack.gif)   ![]_](_urbrack.gif)    |
|
Theorem | sbceq2g 3158* |
Move proper substitution to second argument of an equality.
(Contributed by NM, 30-Nov-2005.)
|
    ![]. ].](_drbrack.gif)
  ![]_](_urbrack.gif)    |
|
Theorem | csbcomg 3159* |
Commutative law for double substitution into a class. (Contributed by
NM, 14-Nov-2005.)
|
     ![]_](_urbrack.gif)   ![]_](_urbrack.gif)   ![]_](_urbrack.gif)   ![]_](_urbrack.gif)   |
|
Theorem | csbeq2d 3160 |
Formula-building deduction rule for class substitution. (Contributed by
NM, 22-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
       ![]_](_urbrack.gif)   ![]_](_urbrack.gif)   |
|
Theorem | csbeq2dv 3161* |
Formula-building deduction rule for class substitution. (Contributed by
NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
     ![]_](_urbrack.gif)   ![]_](_urbrack.gif)   |
|
Theorem | csbeq2i 3162 |
Formula-building inference rule for class substitution. (Contributed by
NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
  ![]_](_urbrack.gif)
  ![]_](_urbrack.gif)  |
|
Theorem | csbvarg 3163 |
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 3164* |
Substitution into a wff expressed in terms of substitution into a
class. (Contributed by NM, 15-Aug-2007.)
|
    ![]. ].](_drbrack.gif)
  ![]_](_urbrack.gif) 
    |
|
Theorem | sbccsb2g 3165 |
Substitution into a wff expressed in using substitution into a class.
(Contributed by NM, 27-Nov-2005.)
|
    ![]. ].](_drbrack.gif)
  ![]_](_urbrack.gif) 
    |
|
Theorem | nfcsb1d 3166 |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12-Oct-2016.)
|
         ![]_](_urbrack.gif)   |
|
Theorem | nfcsb1 3167 |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12-Oct-2016.)
|
      ![]_](_urbrack.gif)  |
|
Theorem | nfcsb1v 3168* |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro,
12-Oct-2016.)
|
    ![]_](_urbrack.gif)  |
|
Theorem | nfcsbd 3169 |
Deduction version of nfcsb 3170. (Contributed by NM, 21-Nov-2005.)
(Revised by Mario Carneiro, 12-Oct-2016.)
|
               ![]_](_urbrack.gif)   |
|
Theorem | nfcsb 3170 |
Bound-variable hypothesis builder for substitution into a class.
(Contributed by Mario Carneiro, 12-Oct-2016.)
|
        ![]_](_urbrack.gif)  |
|
Theorem | csbhypf 3171* |
Introduce an explicit substitution into an implicit substitution
hypothesis. See sbhypf 2904 for class substitution version. (Contributed
by NM, 19-Dec-2008.)
|
    
    ![]_](_urbrack.gif)   |
|
Theorem | csbiebt 3172* |
Conversion of implicit substitution to explicit substitution into a
class. (Closed theorem version of csbiegf 3176.) (Contributed by NM,
11-Nov-2005.)
|
            ![]_](_urbrack.gif)    |
|
Theorem | csbiedf 3173* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by Mario Carneiro, 13-Oct-2016.)
|
               ![]_](_urbrack.gif)   |
|
Theorem | csbieb 3174* |
Bidirectional conversion between an implicit class substitution
hypothesis
and its explicit
substitution equivalent.
(Contributed by NM, 2-Mar-2008.)
|
         ![]_](_urbrack.gif)   |
|
Theorem | csbiebg 3175* |
Bidirectional conversion between an implicit class substitution
hypothesis
and its explicit
substitution equivalent.
(Contributed by NM, 24-Mar-2013.) (Revised by Mario Carneiro,
11-Dec-2016.)
|
          ![]_](_urbrack.gif)    |
|
Theorem | csbiegf 3176* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by NM, 11-Nov-2005.) (Revised by Mario Carneiro,
13-Oct-2016.)
|
    
 
  ![]_](_urbrack.gif)   |
|
Theorem | csbief 3177* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro,
13-Oct-2016.)
|
  
   ![]_](_urbrack.gif)  |
|
Theorem | csbied 3178* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario
Carneiro, 13-Oct-2016.)
|
         ![]_](_urbrack.gif)   |
|
Theorem | csbied2 3179* |
Conversion of implicit substitution to explicit class substitution,
deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)
|
           ![]_](_urbrack.gif)   |
|
Theorem | csbie2t 3180* |
Conversion of implicit substitution to explicit substitution into a
class (closed form of csbie2 3181). (Contributed by NM, 3-Sep-2007.)
(Revised by Mario Carneiro, 13-Oct-2016.)
|
           ![]_](_urbrack.gif)   ![]_](_urbrack.gif)   |
|
Theorem | csbie2 3181* |
Conversion of implicit substitution to explicit substitution into a
class. (Contributed by NM, 27-Aug-2007.)
|
 
    ![]_](_urbrack.gif)   ![]_](_urbrack.gif)
 |
|
Theorem | csbie2g 3182* |
Conversion of implicit substitution to explicit class substitution.
This version of sbcie 3080 avoids a disjointness condition on  by
substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016.)
|
  
 
  ![]_](_urbrack.gif)   |
|
Theorem | sbcnestgf 3183 |
Nest the composition of two substitutions. (Contributed by Mario
Carneiro, 11-Nov-2016.)
|
          ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    ![]_](_urbrack.gif)  ![]. ].](_drbrack.gif)    |
|
Theorem | csbnestgf 3184 |
Nest the composition of two substitutions. (Contributed by NM,
23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
|
         ![]_](_urbrack.gif)   ![]_](_urbrack.gif)    ![]_](_urbrack.gif)  ![]_](_urbrack.gif)   |
|
Theorem | sbcnestg 3185* |
Nest the composition of two substitutions. (Contributed by NM,
27-Nov-2005.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
|
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
   ![]_](_urbrack.gif)  ![]. ].](_drbrack.gif)    |
|
Theorem | csbnestg 3186* |
Nest the composition of two substitutions. (Contributed by NM,
23-Nov-2005.) (Proof shortened by Mario Carneiro, 10-Nov-2016.)
|
   ![]_](_urbrack.gif)   ![]_](_urbrack.gif)
   ![]_](_urbrack.gif)  ![]_](_urbrack.gif)   |
|
Theorem | csbnestgOLD 3187* |
Nest the composition of two substitutions. (New usage is discouraged.)
(Contributed by NM, 23-Nov-2005.)
|
      ![]_](_urbrack.gif)   ![]_](_urbrack.gif)    ![]_](_urbrack.gif)  ![]_](_urbrack.gif)   |
|
Theorem | csbnest1g 3188 |
Nest the composition of two substitutions. (Contributed by NM,
23-May-2006.) (Proof shortened by Mario Carneiro, 11-Nov-2016.)
|
   ![]_](_urbrack.gif)   ![]_](_urbrack.gif)
   ![]_](_urbrack.gif)  ![]_](_urbrack.gif)   |
|
Theorem | csbnest1gOLD 3189* |
Nest the composition of two substitutions. Obsolete as of 11-Nov-2016.
(Contributed by NM, 23-May-2006.) (New usage is discouraged.)
|
      ![]_](_urbrack.gif)   ![]_](_urbrack.gif)    ![]_](_urbrack.gif)  ![]_](_urbrack.gif)   |
|
Theorem | csbidmg 3190* |
Idempotent law for class substitutions. (Contributed by NM,
1-Mar-2008.)
|
   ![]_](_urbrack.gif)   ![]_](_urbrack.gif)
  ![]_](_urbrack.gif)   |
|
Theorem | sbcco3g 3191* |
Composition of two substitutions. (Contributed by NM, 27-Nov-2005.)
(Revised by Mario Carneiro, 11-Nov-2016.)
|
  
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)    |
|
Theorem | sbcco3gOLD 3192* |
Composition of two substitutions. (Contributed by NM, 27-Nov-2005.)
(New usage is discouraged.)
|
    

   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
|
Theorem | csbco3g 3193* |
Composition of two class substitutions. (Contributed by NM,
27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
|
  
  ![]_](_urbrack.gif)   ![]_](_urbrack.gif)
  ![]_](_urbrack.gif)   |
|
Theorem | csbco3gOLD 3194* |
Composition of two class substitutions. Obsolete as of 11-Nov-2016.
(Contributed by NM, 27-Nov-2005.) (New usage is discouraged.)
|
    

  ![]_](_urbrack.gif)   ![]_](_urbrack.gif)   ![]_](_urbrack.gif)   |
|
Theorem | rspcsbela 3195* |
Special case related to rspsbc 3124. (Contributed by NM, 10-Dec-2005.)
(Proof shortened by Eric Schmidt, 17-Jan-2007.)
|
      ![]_](_urbrack.gif)   |
|
Theorem | sbnfc2 3196* |
Two ways of expressing " is (effectively) not free in ."
(Contributed by Mario Carneiro, 14-Oct-2016.)
|
         ![]_](_urbrack.gif)   ![]_](_urbrack.gif)   |
|
Theorem | csbabg 3197* |
Move substitution into a class abstraction. (Contributed by NM,
13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|
   ![]_](_urbrack.gif) 
    ![]. ].](_drbrack.gif)    |
|
Theorem | cbvralcsf 3198 |
A more general version of cbvralf 2829 that doesn't require and
to be distinct from or .
Changes bound variables using
implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.)
|
        
 
        |
|
Theorem | cbvrexcsf 3199 |
A more general version of cbvrexf 2830 that has no distinct variable
restrictions. Changes bound variables using implicit substitution.
(Contributed by Andrew Salmon, 13-Jul-2011.) (Proof shortened by Mario
Carneiro, 7-Dec-2014.)
|
        
 
        |
|
Theorem | cbvreucsf 3200 |
A more general version of cbvreuv 2837 that has no distinct variable
rextrictions. Changes bound variables using implicit substitution.
(Contributed by Andrew Salmon, 13-Jul-2011.)
|
        
 
        |