Theorem List for Metamath Proof Explorer - 37201-37300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 3impcombi 37201 |
A 1-hypothesis propositional calculus deduction. (Contributed by Alan
Sare, 25-Sep-2017.)
|
 

        |
|
Theorem | 3imp231 37202 |
Importation inference. (Contributed by Alan Sare, 17-Oct-2017.)
|
  
        |
|
21.29.6 Theorems proved using Virtual
Deduction
|
|
Theorem | trsspwALT 37203 |
Virtual deduction proof of the left-to-right implication of dftr4 4474. A
transitive class is a subset of its power class. This proof corresponds
to the virtual deduction proof of dftr4 4474 without accumulating results.
(Contributed by Alan Sare, 29-Apr-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|

   |
|
Theorem | trsspwALT2 37204 |
Virtual deduction proof of trsspwALT 37203. This proof is the same as the
proof of trsspwALT 37203 except each virtual deduction symbol is
replaced by
its non-virtual deduction symbol equivalent. A transitive class is a
subset of its power class. (Contributed by Alan Sare, 23-Jul-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|

   |
|
Theorem | trsspwALT3 37205 |
Short predicate calculus proof of the left-to-right implication of
dftr4 4474. A transitive class is a subset of its power
class. This
proof was constructed by applying Metamath's minimize command to the
proof of trsspwALT2 37204, which is the virtual deduction proof trsspwALT 37203
without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|

   |
|
Theorem | sspwtr 37206 |
Virtual deduction proof of the right-to-left implication of dftr4 4474. A
class which is a subclass of its power class is transitive. This proof
corresponds to the virtual deduction proof of sspwtr 37206 without
accumulating results. (Contributed by Alan Sare, 2-May-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
    |
|
Theorem | sspwtrALT 37207 |
Virtual deduction proof of sspwtr 37206. This proof is the same as the
proof of sspwtr 37206 except each virtual deduction symbol is
replaced by
its non-virtual deduction symbol equivalent. A class which is a
subclass of its power class is transitive. (Contributed by Alan Sare,
3-May-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
    |
|
Theorem | csbabgOLD 37208* |
Move substitution into a class abstraction. (Contributed by NM,
13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) Obsolete
as of 19-Aug-2018. Use csbab 3765 instead. (New usage is discouraged.)
(Proof modification is discouraged.)
|

  ![]_ ]_](_urbrack.gif) 
 
  ![]. ].](_drbrack.gif)    |
|
Theorem | csbunigOLD 37209 |
Distribute proper substitution through the union of a class.
(Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 22-Aug-2018.
Use csbuni 4196 instead. (New usage is discouraged.)
(Proof modification is discouraged.)
|

  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
|
Theorem | csbfv12gALTOLD 37210 |
Move class substitution in and out of a function value. The proof is
derived from the virtual deduction proof csbfv12gALTVD 37293. (Contributed
by Alan Sare, 10-Nov-2012.) Obsolete as of 20-Aug-2018. Use csbfv12 5883
instead. (Proof modification is discouraged.)
(New usage is discouraged.)
|

  ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    |
|
Theorem | csbxpgOLD 37211 |
Distribute proper substitution through the Cartesian product of two
classes. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of
23-Aug-2018. Use csbrn 5276 instead. (New usage is discouraged.)
(Proof modification is discouraged.)
|

  ![]_ ]_](_urbrack.gif) 
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
|
Theorem | csbingOLD 37212 |
Distribute proper substitution through an intersection relation.
(Contributed by Alan Sare, 22-Jul-2012.) Obsolete as of 18-Aug-2018.
Use csbin 3767 instead. (New usage is discouraged.)
(Proof modification is discouraged.)
|

  ![]_ ]_](_urbrack.gif) 
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
|
Theorem | csbresgOLD 37213 |
Distribute proper substitution through the restriction of a class.
csbresgOLD 37213 is derived from the virtual deduction proof
csbresgVD 37289.
(Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 23-Aug-2018. Use
csbres 5086 instead. (New usage is discouraged.)
(Proof modification is discouraged.)
|

  ![]_ ]_](_urbrack.gif) 
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
|
Theorem | csbrngOLD 37214 |
Distribute proper substitution through the range of a class.
(Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 23-Aug-2018.
Use csbrn 5276 instead. (New usage is discouraged.)
(Proof modification is discouraged.)
|

  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
|
Theorem | csbima12gALTOLD 37215 |
Move class substitution in and out of the image of a function. The proof
is derived from the virtual deduction proof csbima12gALTVD 37291.
(Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 20-Aug-2018. Use
csbfv12 5883 instead. (Proof modification is
discouraged.) (Proof
modification is discouraged.) (New usage is discouraged.)
|

  ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)    |
|
Theorem | sspwtrALT2 37216 |
Short predicate calculus proof of the right-to-left implication of
dftr4 4474. A class which is a subclass of its power
class is
transitive. This proof was constructed by applying Metamath's minimize
command to the proof of sspwtrALT 37207, which is the virtual deduction
proof sspwtr 37206 without virtual deductions. (Contributed by
Alan Sare,
3-May-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
    |
|
Theorem | pwtrVD 37217 |
Virtual deduction proof of pwtr 4626; see pwtrrVD 37218 for the converse.
(Contributed by Alan Sare, 25-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|

   |
|
Theorem | pwtrrVD 37218 |
Virtual deduction proof of pwtr 4626; see pwtrVD 37217 for the converse.
(Contributed by Alan Sare, 25-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
    |
|
Theorem | suctrALT 37219 |
The successor of a transitive class is transitive. The proof of
http://us.metamath.org/other/completeusersproof/suctrvd.html
is a
Virtual Deduction proof verified by automatically transforming it into
the Metamath proof of suctrALT 37219 using completeusersproof, which is
verified by the Metamath program. The proof of
http://us.metamath.org/other/completeusersproof/suctrro.html
is a form
of the completed proof which preserves the Virtual Deduction proof's
step numbers and their ordering. See suctr 5485 for the original proof.
(Contributed by Alan Sare, 11-Apr-2009.) (Revised by Alan Sare,
12-Jun-2018.) (Proof modification is discouraged.)
(New usage is discouraged.)
|

  |
|
Theorem | snssiALTVD 37220 |
Virtual deduction proof of snssiALT 37221. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|

    |
|
Theorem | snssiALT 37221 |
If a class is an element of another class, then its singleton is a
subclass of that other class. Alternate proof of snssi 4085. This
theorem was automatically generated from snssiALTVD 37220 using a
translation program. (Contributed by Alan Sare, 11-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|

    |
|
Theorem | snsslVD 37222 |
Virtual deduction proof of snssl 37223. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
  
  |
|
Theorem | snssl 37223 |
If a singleton is a subclass of another class, then the singleton's
element is an element of that other class. This theorem is the
right-to-left implication of the biconditional snss 4065.
The proof of
this theorem was automatically generated from snsslVD 37222 using a tools
command file, translateMWO.cmd, by translating the proof into its
non-virtual deduction form and minimizing it. (Contributed by Alan
Sare, 25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
  
  |
|
Theorem | snelpwrVD 37224 |
Virtual deduction proof of snelpwi 4618. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|

     |
|
Theorem | unipwrVD 37225 |
Virtual deduction proof of unipwr 37226. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
   |
|
Theorem | unipwr 37226 |
A class is a subclass of the union of its power class. This theorem is
the right-to-left subclass lemma of unipw 4623. The proof of this theorem
was automatically generated from unipwrVD 37225 using a tools command file ,
translateMWO.cmd , by translating the proof into its non-virtual
deduction form and minimizing it. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
   |
|
Theorem | sstrALT2VD 37227 |
Virtual deduction proof of sstrALT2 37228. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
 

  |
|
Theorem | sstrALT2 37228 |
Virtual deduction proof of sstr 3408, transitivity of subclasses, Theorem
6 of [Suppes] p. 23. This theorem was
automatically generated from
sstrALT2VD 37227 using the command file translatewithout_overwriting.cmd .
It was not minimized because the automated minimization excluding
duplicates generates a minimized proof which, although not directly
containing any duplicates, indirectly contains a duplicate. That is,
the trace back of the minimized proof contains a duplicate. This is
undesirable because some step(s) of the minimized proof use the proven
theorem. (Contributed by Alan Sare, 11-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
 

  |
|
Theorem | suctrALT2VD 37229 |
Virtual deduction proof of suctrALT2 37230. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|

  |
|
Theorem | suctrALT2 37230 |
Virtual deduction proof of suctr 5485. The sucessor of a transitive class
is transitive. This proof was generated automatically from the virtual
deduction proof suctrALT2VD 37229 using the tools command file
translatewithout_overwritingminimize_excludingduplicates.cmd .
(Contributed by Alan Sare, 11-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|

  |
|
Theorem | elex2VD 37231* |
Virtual deduction proof of elex2 3026. (Contributed by Alan Sare,
25-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|

   |
|
Theorem | elex22VD 37232* |
Virtual deduction proof of elex22 3027. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
         |
|
Theorem | eqsbc3rVD 37233* |
Virtual deduction proof of eqsbc3r 3292. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|

   ![]. ].](_drbrack.gif)
   |
|
Theorem | zfregs2VD 37234* |
Virtual deduction proof of zfregs2 8204. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|

   
   |
|
Theorem | tpid3gVD 37235 |
Virtual deduction proof of tpid3g 4056. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|

  
   |
|
Theorem | en3lplem1VD 37236* |
Virtual deduction proof of en3lplem1 8106. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
 
       

    |
|
Theorem | en3lplem2VD 37237* |
Virtual deduction proof of en3lplem2 8107. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
 
   
 
    
 
    |
|
Theorem | en3lpVD 37238 |
Virtual deduction proof of en3lp 8108. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|

  |
|
21.29.7 Theorems proved using Virtual Deduction
with mmj2 assistance
|
|
Theorem | simplbi2VD 37239 |
Virtual deduction proof of simplbi2 635. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
h1:: |    
| 3:1,?: e0a 37156 |    
| qed:3,?: e0a 37156 |    
|
The proof of simplbi2 635 was automatically derived from it.
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
         |
|
Theorem | 3ornot23VD 37240 |
Virtual deduction proof of 3ornot23 36866. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1::    
 
| 2:: |      
   
| 3:1,?: e1a 37006 |    
| 4:1,?: e1a 37006 |    
| 5:3,4,?: e11 37067 |    
 
| 6:2,?: e2 37010 |      
     
| 7:5,6,?: e12 37108 |      
 
| 8:7: |     
  
| qed:8: |     
  
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
  
 
    |
|
Theorem | orbi1rVD 37241 |
Virtual deduction proof of orbi1r 36867. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |      
| 2:: |       
  
| 3:2,?: e2 37010 |       
  
| 4:1,3,?: e12 37108 |       
  
| 5:4,?: e2 37010 |       
  
| 6:5: |      
   
| 7:: |       
  
| 8:7,?: e2 37010 |       
  
| 9:1,8,?: e12 37108 |       
  
| 10:9,?: e2 37010 |       
  
| 11:10: |      
   
| 12:6,11,?: e11 37067 |     
    
| qed:12: |      
   
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 
         |
|
Theorem | bitr3VD 37242 |
Virtual deduction proof of bitr3 36868. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |    
 
| 2:1,?: e1a 37006 |    
 
| 3:: |       
  
| 4:3,?: e2 37010 |       
  
| 5:2,4,?: e12 37108 |       
  
| 6:5: |     
    
| qed:6: |      
   
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 
  
      |
|
Theorem | 3orbi123VD 37243 |
Virtual deduction proof of 3orbi123 36869. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |      
       
   
| 2:1,?: e1a 37006 |      
     
| 3:1,?: e1a 37006 |      
     
| 4:1,?: e1a 37006 |      
     
| 5:2,3,?: e11 37067 |      
         
| 6:5,4,?: e11 37067 |      
          
  
| 7:?: |      
 
| 8:6,7,?: e10 37073 |      
        
  
| 9:?: |     
  
| 10:8,9,?: e10 37073 |     
       
  
| qed:10: |      
      
  
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
                 |
|
Theorem | sbc3orgVD 37244 |
Virtual deduction proof of sbc3orgOLD 36894. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |  
| 2:1,?: e1a 37006 |     ![]. ].](_drbrack.gif)  
     ![]. ].](_drbrack.gif)  
  ![]. ].](_drbrack.gif)   
| 3:: |      
 
| 32:3: |       
  
| 33:1,32,?: e10 37073 |    ![]. ].](_drbrack.gif)   
     
| 4:1,33,?: e11 37067 |     ![]. ].](_drbrack.gif)  
    ![]. ].](_drbrack.gif)    
| 5:2,4,?: e11 37067 |     ![]. ].](_drbrack.gif) 
    ![]. ].](_drbrack.gif)     ![]. ].](_drbrack.gif)   
| 6:1,?: e1a 37006 |     ![]. ].](_drbrack.gif) 
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   
| 7:6,?: e1a 37006 |      ![]. ].](_drbrack.gif) 
   ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
  ![]. ].](_drbrack.gif)   
| 8:5,7,?: e11 37067 |     ![]. ].](_drbrack.gif) 
     ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
  ![]. ].](_drbrack.gif)   
| 9:?: |      ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)    ![]. ].](_drbrack.gif)     ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
| 10:8,9,?: e10 37073 |     ![]. ].](_drbrack.gif) 
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)   
| qed:10: |     ![]. ].](_drbrack.gif) 
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)   
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|

   ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
|
Theorem | 19.21a3con13vVD 37245* |
Virtual deduction proof of alrim3con13v 36895. The following user's
proof is completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
1:: |     
    
| 2:: |        
   
| 3:2,?: e2 37010 |        
 
| 4:2,?: e2 37010 |        
 
| 5:2,?: e2 37010 |        
 
| 6:1,4,?: e12 37108 |        
   
| 7:3,?: e2 37010 |        
   
| 8:5,?: e2 37010 |        
   
| 9:7,6,8,?: e222 37015 |        
         
| 10:9,?: e2 37010 |        
     
| 11:10:in2 |       
      
| qed:11:in1 |       
      
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 
  
 
        |
|
Theorem | exbirVD 37246 |
Virtual deduction proof of exbir 36834. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |       
      
| 2:: |        
    
| 3:: |        
   
| 5:1,2,?: e12 37108 |     
       
| 6:3,5,?: e32 37142 |     
      
| 7:6: |     
       
| 8:7: |       
      
| 9:8,?: e1a 37006 |     
        
| qed:9: |       
      
|
(Contributed by Alan Sare, 13-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
       
       |
|
Theorem | exbiriVD 37247 |
Virtual deduction proof of exbiri 632. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
h1:: |      
| 2:: |  
| 3:: |    
| 4:: |      
| 5:2,1,?: e10 37073 |      
| 6:3,5,?: e21 37114 |      
| 7:4,6,?: e32 37142 |      
| 8:7: |      
| 9:8: |      
| qed:9: |      
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 
     
     |
|
Theorem | rspsbc2VD 37248* |
Virtual deduction proof of rspsbc2 36896. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |  
| 2:: |    
| 3:: |      
      
| 4:1,3,?: e13 37132 |      
    ![]. ].](_drbrack.gif)   
| 5:1,4,?: e13 37132 |      
      ![]. ].](_drbrack.gif) 
| 6:2,5,?: e23 37139 |      
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
| 7:6: |     
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
| 8:7: |  
       ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   
| qed:8: |  
       ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|

      ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
|
Theorem | 3impexpVD 37249 |
Virtual deduction proof of 3impexp 1234. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |    
     
| 2:: |   
    
| 3:1,2,?: e10 37073 |    
       
| 4:3,?: e1a 37006 |    
       
| 5:4,?: e1a 37006 |    
       
| 6:5: |     
      
| 7:: |    
         
| 8:7,?: e1a 37006 |    
         
| 9:8,?: e1a 37006 |    
         
| 10:2,9,?: e01 37070 |    
       
| 11:10: |    
       
| qed:6,11,?: e00 37152 |    
       
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
       
     |
|
Theorem | 3impexpbicomVD 37250 |
Virtual deduction proof of 3impexpbicom 36835. The following user's proof
is completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
1:: |    
         
| 2:: |    
 
| 3:1,2,?: e10 37073 |    
         
| 4:3,?: e1a 37006 |    
      
    
| 5:4: |    
      
    
| 6:: |    
        
    
| 7:6,?: e1a 37006 |    
        
  
| 8:7,2,?: e10 37073 |    
        
  
| 9:8: |    
        
  
| qed:5,9,?: e00 37152 |    
      
    
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
        
        |
|
Theorem | 3impexpbicomiVD 37251 |
Virtual deduction proof of 3impexpbicomi 36836. The following user's proof
is completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 

            |
|
Theorem | sbcel1gvOLD 37252* |
Class substitution into a membership relation. (Contributed by NM,
17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Obsolete as of 17-Aug-2018. Use sbcel1v 3294 instead.
(New usage is discouraged.) (Proof modification is discouraged.)
|

   ![]. ].](_drbrack.gif)
   |
|
Theorem | sbcoreleleqVD 37253* |
Virtual deduction proof of sbcoreleleq 36897. The following user's proof
is completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
1:: |  
| 2:1,?: e1a 37006 |     ![]. ].](_drbrack.gif)
 
| 3:1,?: e1a 37006 |     ![]. ].](_drbrack.gif)
 
| 4:1,?: e1a 37006 |     ![]. ].](_drbrack.gif)
 
| 5:2,3,4,?: e111 37053 |   
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)   
| 6:1,?: e1a 37006 | 
   ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   
| 7:5,6: e11 37067 |     ![]. ].](_drbrack.gif) 
    
| qed:7: |     ![]. ].](_drbrack.gif) 
    
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|

   ![]. ].](_drbrack.gif) 
 
    |
|
Theorem | hbra2VD 37254* |
Virtual deduction proof of nfra2 2771. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
1:: |     
      
| 2:: |     
    
| 3:1,2,?: e00 37152 |     
      
| 4:2: |       
    
| 5:4,?: e0a 37156 |       
      
| qed:3,5,?: e00 37152 |     
      
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 
       |
|
Theorem | tratrbVD 37255* |
Virtual deduction proof of tratrb 36898. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |   
    
      
 
| 2:1,?: e1a 37006 |   
     
| 3:1,?: e1a 37006 |   
    
      
| 4:1,?: e1a 37006 |   
     
| 5:: |   
      
   
| 6:5,?: e2 37010 |   
      
 
| 7:5,?: e2 37010 |   
      
 
| 8:2,7,4,?: e121 37035 |   
      
 
| 9:2,6,8,?: e122 37032 |   
      
 
| 10:: |   
      
  
| 11:6,7,10,?: e223 37014 |   
      
    
| 12:11: |   
      
     
| 13:: | 

| 14:12,13,?: e20 37111 |   
      
 
| 15:: |   
      
  
| 16:7,15,?: e23 37139 |   
      
  
| 17:6,16,?: e23 37139 |   
      
    
| 18:17: |   
      
     
| 19:: |  
| 20:18,19,?: e20 37111 |   
      
 
| 21:3,?: e1a 37006 |   
     
    
| 22:21,9,4,?: e121 37035 |   
      
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
 
| 23:22,?: e2 37010 |   
      
   ![]. ].](_drbrack.gif)   
| 24:4,23,?: e12 37108 |   
      
   
| 25:14,20,24,?: e222 37015 |   
      
 
| 26:25: |   
      
  
| 27:: |      
       
 
| 28:27,?: e0a 37156 |   
    
       
  
| 29:28,26: |   
    
      
| 30:: |      
       
 
| 31:30,?: e0a 37156 |   
       
       
| 32:31,29: |   
     
      
| 33:32,?: e1a 37006 |   
     
| qed:33: |   
     
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
   

    |
|
Theorem | al2imVD 37256 |
Virtual deduction proof of al2im 1690. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |       
      
| 2:1,?: e1a 37006 |       
        
| 3:: |        
   
| 4:2,3,?: e10 37073 |       
          
| qed:4: |       
          
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
    
 
  
  
      |
|
Theorem | syl5impVD 37257 |
Virtual deduction proof of syl5imp 36870. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: |      
   
| 2:1,?: e1a 37006 |      
   
| 3:: |        
   
| 4:3,2,?: e21 37114 |        
     
| 5:4,?: e2 37010 |        
     
| 6:5: |       
      
| qed:6: |       
      
|
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 
     
       |
|
Theorem | idiVD 37258 |
Virtual deduction proof of idiALT 36833. The following user's
proof is completed by invoking mmj2's unify command and using mmj2's
StepSelector to pick all remaining steps of the Metamath proof.
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 |
|
Theorem | ancomstVD 37259 |
Closed form of ancoms 459. The following user's proof is completed by
invoking mmj2's unify command and using mmj2's StepSelector to pick all
remaining steps of the Metamath proof.
The proof of ancomst 458 is derived automatically from it.
(Contributed by Alan Sare, 25-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
           |
|
Theorem | ssralv2VD 37260* |
Quantification restricted to a subclass for two quantifiers. ssralv 3461
for two quantifiers. The following User's Proof is a Virtual Deduction
proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. ssralv2 36889 is ssralv2VD 37260 without
virtual deductions and was automatically derived from ssralv2VD 37260.
1:: |    
 
| 2:: |      
      
| 3:1: |    
| 4:3,2: |      
      
| 5:4: |      
        
| 6:5: |      
      
| 7:: |      
   
| 8:7,6: |      
     
| 9:1: |    
| 10:9,8: |      
     
| 11:10: |      
      
| 12:: |   
    
| 13:: |     
      
| 14:12,13,11: |      
        
| 15:14: |      
      
| 16:15: |   
          
| qed:16: |   
          
|
(Contributed by Alan Sare, 10-Feb-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 
   
     |
|
Theorem | ordelordALTVD 37261 |
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36. This is an alternate proof of ordelord 5424 using
the Axiom of Regularity indirectly through dford2 8112. dford2 is a
weaker definition of ordinal number. Given the Axiom of Regularity, it
need not be assumed that because this is inferred by the
Axiom of Regularity. The following User's Proof is a Virtual Deduction
proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. ordelordALT 36899 is ordelordALTVD 37261
without virtual deductions and was automatically derived from
ordelordALTVD 37261 using the tools program
translate..without..overwriting.cmd and Metamath's minimize command.
1:: |    
 
| 2:1: |    
| 3:1: |    
| 4:2: |    
| 5:2: |    
    
| 6:4,3: |    
| 7:6,6,5: |    
    
| 8:: |   
  
| 9:8: |     
  
| 10:9: |    
   
| 11:10: |    
     
| 12:11: |      
     
| 13:12: |      
     
| 14:13: |      
     
 
| 15:14,5: |    
    
| 16:4,15,3: |    
| 17:16,7: |    
| qed:17: |    
|
(Contributed by Alan Sare, 12-Feb-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 
   |
|
Theorem | equncomVD 37262 |
If a class equals the union of two other classes, then it equals the
union of those two classes commuted. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. equncom 3547 is equncomVD 37262 without
virtual deductions and was automatically derived from equncomVD 37262.
1:: |      
| 2:: |    
| 3:1,2: |      
| 4:3: |      
| 5:: |      
| 6:5,2: |      
| 7:6: |      
| 8:4,7: |      
|
(Contributed by Alan Sare, 17-Feb-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|

 
    |
|
Theorem | equncomiVD 37263 |
Inference form of equncom 3547. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. equncomi 3548 is equncomiVD 37263 without
virtual deductions and was automatically derived from equncomiVD 37263.
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
     |
|
Theorem | sucidALTVD 37264 |
A set belongs to its successor. Alternate proof of sucid 5481.
The following User's Proof is a Virtual Deduction proof
completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. sucidALT 37265 is sucidALTVD 37264
without virtual deductions and was automatically derived from
sucidALTVD 37264. This proof illustrates that
completeusersproof.cmd will generate a Metamath proof from any
User's Proof which is "conventional" in the sense that no step
is a virtual deduction, provided that all necessary unification
theorems and transformation deductions are in set.mm.
completeusersproof.cmd automatically converts such a
conventional proof into a Virtual Deduction proof for which each
step happens to be a 0-virtual hypothesis virtual deduction.
The user does not need to search for reference theorem labels or
deduction labels nor does he(she) need to use theorems and
deductions which unify with reference theorems and deductions in
set.mm. All that is necessary is that each theorem or deduction
of the User's Proof unifies with some reference theorem or
deduction in set.mm or is a semantic variation of some theorem
or deduction which unifies with some reference theorem or
deduction in set.mm. The definition of "semantic variation" has
not been precisely defined. If it is obvious that a theorem or
deduction has the same meaning as another theorem or deduction,
then it is a semantic variation of the latter theorem or
deduction. For example, step 4 of the User's Proof is a
semantic variation of the definition (axiom)
    , which unifies with df-suc 5408, a
reference definition (axiom) in set.mm. Also, a theorem or
deduction is said to be a semantic variation of another
theorem or deduction if it is obvious upon cursory inspection
that it has the same meaning as a weaker form of the latter
theorem or deduction. For example, the deduction
infers       is a
semantic variation of the theorem   
      , which unifies with
the set.mm reference definition (axiom) dford2 8112.
h1:: |
| 2:1: |  
| 3:2: |    
| 4:: |    
| qed:3,4: |
|
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 |
|
Theorem | sucidALT 37265 |
A set belongs to its successor. This proof was automatically derived
from sucidALTVD 37264 using translatewithout_overwriting.cmd and
minimizing. (Contributed by Alan Sare, 18-Feb-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
 |
|
Theorem | sucidVD 37266 |
A set belongs to its successor. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools
program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2
and Norm Megill's Metamath Proof Assistant.
sucid 5481 is sucidVD 37266 without virtual deductions and was automatically
derived from sucidVD 37266.
h1:: |
| 2:1: |  
| 3:2: |    
| 4:: |    
| qed:3,4: |
|
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 |
|
Theorem | imbi12VD 37267 |
Implication form of imbi12i 332.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
imbi12 328 is imbi12VD 37267 without virtual deductions and was automatically
derived from imbi12VD 37267.
1:: |      
| 2:: |       
  
| 3:: |          
   
| 4:1,3: |          
   
| 5:2,4: |          
   
| 6:5: |       
      
| 7:: |          
   
| 8:1,7: |          
   
| 9:2,8: |          
   
| 10:9: |       
      
| 11:6,10: |       
      
| 12:11: |      
       
| qed:12: |      
       
|
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 
     
 
     |
|
Theorem | imbi13VD 37268 |
Join three logical equivalences to form equivalence of implications.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
imbi13 36878 is imbi13VD 37268 without virtual deductions and was automatically
derived from imbi13VD 37268.
1:: |      
| 2:: |       
  
| 3:: |          
   
| 4:2,3: |          
       
| 5:1,4: |          
           
| 6:5: |       
         
    
| 7:6: |      
         
     
| qed:7: |      
         
     
|
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 
        
    
       |
|
Theorem | sbcim2gVD 37269 |
Distribution of class substitution over a left-nested implication.
Similar to sbcimg 3277.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
sbcim2g 36900 is sbcim2gVD 37269 without virtual deductions and was automatically
derived from sbcim2gVD 37269.
1:: |  
| 2:: |      ![]. ].](_drbrack.gif)  
    ![]. ].](_drbrack.gif)     
| 3:1,2: |      ![]. ].](_drbrack.gif)  
     ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    
| 4:1: |     ![]. ].](_drbrack.gif)  
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   
| 5:3,4: |      ![]. ].](_drbrack.gif)  
     ![]. ].](_drbrack.gif)    ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)   
| 6:5: |     ![]. ].](_drbrack.gif)  
     ![]. ].](_drbrack.gif)    ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)    
| 7:: |       ![]. ].](_drbrack.gif)
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   
| 8:4,7: |       ![]. ].](_drbrack.gif)
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)    
| 9:1: |     ![]. ].](_drbrack.gif)  
     ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     
| 10:8,9: |       ![]. ].](_drbrack.gif)
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     ![]. ].](_drbrack.gif)  
  
| 11:10: |      ![]. ].](_drbrack.gif)
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     ![]. ].](_drbrack.gif)  
   
| 12:6,11: |     ![]. ].](_drbrack.gif) 
      ![]. ].](_drbrack.gif)    ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)    
| qed:12: |     ![]. ].](_drbrack.gif)  
     ![]. ].](_drbrack.gif)    ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)    
|
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|

   ![]. ].](_drbrack.gif)        ![]. ].](_drbrack.gif)    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)      |
|
Theorem | sbcbiVD 37270 |
Implication form of sbcbiiOLD 36893.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
sbcbi 36901 is sbcbiVD 37270 without virtual deductions and was automatically
derived from sbcbiVD 37270.
1:: |  
| 2:: |       
    
| 3:1,2: |       
  ![]. ].](_drbrack.gif)   
| 4:1,3: |       
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)  
| 5:4: |      
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   
| qed:5: |      
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   
|
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|

        ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
|
Theorem | trsbcVD 37271* |
Formula-building inference rule for class substitution, substituting a
class variable for the setvar variable of the transitivity predicate.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
trsbc 36902 is trsbcVD 37271 without virtual deductions and was automatically
derived from trsbcVD 37271.
1:: |  
| 2:1: |     ![]. ].](_drbrack.gif)
 
| 3:1: |     ![]. ].](_drbrack.gif)
 
| 4:1: |     ![]. ].](_drbrack.gif)
 
| 5:1,2,3,4: |      ![]. ].](_drbrack.gif)
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   
    
| 6:1: |     ![]. ].](_drbrack.gif) 
      ![]. ].](_drbrack.gif)
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    
| 7:5,6: |     ![]. ].](_drbrack.gif) 
    
   
| 8:: |   
      
| 9:7,8: |     ![]. ].](_drbrack.gif) 
     
  
| 10:: |   
      
| 11:10: |     
      
| 12:1,11: |     ![]. ].](_drbrack.gif) 
     ![]. ].](_drbrack.gif)   
  
| 13:9,12: |     ![]. ].](_drbrack.gif)  
    
  
| 14:13: |       ![]. ].](_drbrack.gif)  
    
  
| 15:14: |       ![]. ].](_drbrack.gif)  
      
  
| 16:1: |     ![]. ].](_drbrack.gif)    
      ![]. ].](_drbrack.gif)  
   
| 17:15,16: |     ![]. ].](_drbrack.gif)    
      
  
| 18:17: |       ![]. ].](_drbrack.gif)   
      
  
| 19:18: |       ![]. ].](_drbrack.gif)   
       
   
| 20:1: |     ![]. ].](_drbrack.gif)     
      ![]. ].](_drbrack.gif)    
   
| 21:19,20: |     ![]. ].](_drbrack.gif)     
       
   
| 22:: |       
  
| 23:21,22: |     ![]. ].](_drbrack.gif)     
   
| 24:: |       
  
| 25:24: |         
  
| 26:1,25: |     ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)          
| 27:23,26: |     ![]. ].](_drbrack.gif)
 
| qed:27: |     ![]. ].](_drbrack.gif)
 
|
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|

   ![]. ].](_drbrack.gif)    |
|
Theorem | truniALTVD 37272* |
The union of a class of transitive sets is transitive.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
truniALT 36903 is truniALTVD 37272 without virtual deductions and was
automatically derived from truniALTVD 37272.
1:: |    

| 2:: |      
     
| 3:2: |      
  
| 4:2: |      
   
| 5:4: |      
      
| 6:: |      
       
| 7:6: |      
     
| 8:6: |      
     
| 9:1,8: |      
       ![] ]](rbrack.gif) 
| 10:8,9: |      
     
| 11:3,7,10: |      
     
| 12:11,8: |      
      
| 13:12: |      
       
| 14:13: |      
         
| 15:14: |      
         
| 16:5,15: |      
   
| 17:16: |     
    
| 18:17: |   
          
| 19:18: |     
| qed:19: |     
|
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 
   |
|
Theorem | ee33VD 37273 |
Non-virtual deduction form of e33 37118.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
ee33 36879 is ee33VD 37273 without virtual deductions and was automatically
derived from ee33VD 37273.
h1:: |      
| h2:: |      
| h3:: |    
| 4:1,3: |        
| 5:4: |        
| 6:2,5: |     
      
| 7:6: |     
    
| 8:7: |        
| qed:8: |      
|
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
  
    
    
    
     |
|
Theorem | trintALTVD 37274* |
The intersection of a class of transitive sets is transitive. Virtual
deduction proof of trintALT 37275.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
trintALT 37275 is trintALTVD 37274 without virtual deductions and was
automatically derived from trintALTVD 37274.
1:: |      
| 2:: |      
     
| 3:2: |      
  
| 4:2: |      
   
| 5:4: |      
    
| 6:5: |      
    
| 7:: |      
   
| 8:7,6: |      
   
| 9:7,1: |      
     ![] ]](rbrack.gif) 
| 10:7,9: |      
   
| 11:10,3,8: |      
   
| 12:11: |      
    
| 13:12: |      
      
| 14:13: |      
    
| 15:3,14: |      
   
| 16:15: |     
    
| 17:16: |         
    
| 18:17: |     
| qed:18: |     
|
(Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
 
   |
|
Theorem | trintALT 37275* |
The intersection of a class of transitive sets is transitive. Exercise
5(b) of [Enderton] p. 73. trintALT 37275 is an alternate proof of trint 4484.
trintALT 37275 is trintALTVD 37274 without virtual deductions and was
automatically derived from trintALTVD 37274 using the tools program
translate..without..overwriting.cmd and Metamath's minimize command.
(Contributed by Alan Sare, 17-Apr-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
 
   |
|
Theorem | undif3VD 37276 |
The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual
deduction proof of undif3 3672.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
undif3 3672 is undif3VD 37276 without virtual deductions and was automatically
derived from undif3VD 37276.
1:: |      
   
| 2:: |    
 
| 3:2: |      
   
| 4:1,3: |      
   
| 5:: |  
| 6:5: |    
| 7:5: |    
| 8:6,7: |    
   
| 9:8: |    
  
| 10:: |    
 
| 11:10: |    
| 12:10: |   
| 13:11: |    
 
| 14:12: |    
 
| 15:13,14: |     
    
| 16:15: |     
    
| 17:9,16: |     
      
| 18:: |    
 
| 19:18: |    
| 20:18: |   
| 21:18: |    
   
| 22:21: |    
   
| 23:: |    
 
| 24:23: |    
| 25:24: |    
   
| 26:25: |    
  
| 27:10: |    
   
| 28:27: |    
   
| 29:: |    
 
| 30:29: |    
| 31:30: |    
   
| 32:31: |    
  
| 33:22,26: |     
      
| 34:28,32: |     
      
| 35:33,34: |      
        
    
| 36:: |      
        
      
| 37:36,35: |     
      
| 38:17,37: |     
      
| 39:: |    
 
| 40:39: |    
 
| 41:: |    
 
| 42:40,41: |    
 
| 43:: |    

| 44:43,42: |      
      
| 45:: |       
     
| 46:45,44: |       
     
| 47:4,38: |       
    
| 48:46,47: |       
    
| 49:48: |       
      
| qed:49: |        
 
|
(Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
      
    |
|
Theorem | sbcssgVD 37277 |
Virtual deduction proof of sbcssg 3848.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
sbcssg 3848 is sbcssgVD 37277 without virtual deductions and was automatically
derived from sbcssgVD 37277.
1:: |  
| 2:1: |     ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)  
| 3:1: |     ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)  
| 4:2,3: |      ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
 
| 5:1: |     ![]. ].](_drbrack.gif) 
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   
| 6:4,5: |     ![]. ].](_drbrack.gif) 
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   
| 7:6: |       ![]. ].](_drbrack.gif) 
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   
| 8:7: |       ![]. ].](_drbrack.gif) 
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif) 

| 9:1: |     ![]. ].](_drbrack.gif)   
     ![]. ].](_drbrack.gif)    
| 10:8,9: |     ![]. ].](_drbrack.gif)   
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif) 

| 11:: |      
| 110:11: |      
 
| 12:1,110: |     ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)      
| 13:10,12: |     ![]. ].](_drbrack.gif)
     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   
| 14:: |    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  
| 15:13,14: |     ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  
| qed:15: |     ![]. ].](_drbrack.gif)
 ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  
|
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|

   ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
|
Theorem | csbingVD 37278 |
Virtual deduction proof of csbingOLD 37212.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
csbingOLD 37212 is csbingVD 37278 without virtual deductions and was
automatically derived from csbingVD 37278.
1:: |  
| 2:: |     
| 20:2: |      
 
| 30:1,20: |    ![]. ].](_drbrack.gif)  
    
| 3:1,30: |    ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)     
| 4:1: |    ![]_ ]_](_urbrack.gif)  
     ![]. ].](_drbrack.gif)    
| 5:3,4: |    ![]_ ]_](_urbrack.gif)  
   ![]. ].](_drbrack.gif)    
| 6:1: |     ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)  
| 7:1: |     ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)  
| 8:6,7: |      ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif) 

| 9:1: |     ![]. ].](_drbrack.gif) 
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   
| 10:9,8: |     ![]. ].](_drbrack.gif) 
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   
| 11:10: |       ![]. ].](_drbrack.gif) 
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   
| 12:11: |     ![]. ].](_drbrack.gif) 
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   
| 13:5,12: |    ![]_ ]_](_urbrack.gif)  
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   
| 14:: |    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif) 
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  
| 15:13,14: |    ![]_ ]_](_urbrack.gif)  
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  
| qed:15: |    ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  
|
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is
discouraged.) (New usage is discouraged.)
|

  ![]_ ]_](_urbrack.gif) 
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
|
Theorem | onfrALTlem5VD 37279* |
Virtual deduction proof of onfrALTlem5 36909.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
onfrALTlem5 36909 is onfrALTlem5VD 37279 without virtual deductions and was
automatically derived from onfrALTlem5VD 37279.
1:: |
| 2:1: |  
| 3:2: |      ![]. ].](_drbrack.gif) 
 
| 4:3: |      ![]. ].](_drbrack.gif)
  
| 5:: |    

| 6:4,5: |      ![]. ].](_drbrack.gif)
  
| 7:2: |      ![]. ].](_drbrack.gif)
    ![]. ].](_drbrack.gif) 
| 8:: |  
| 9:8: |    
| 10:2,9: |      ![]. ].](_drbrack.gif)
    ![]. ].](_drbrack.gif) 
| 11:7,10: |      ![]. ].](_drbrack.gif)
    ![]. ].](_drbrack.gif) 
| 12:6,11: |      ![]. ].](_drbrack.gif)
 
| 13:2: |      ![]. ].](_drbrack.gif) 
    
| 14:12,13: |       ![]. ].](_drbrack.gif) 
     ![]. ].](_drbrack.gif)     
    
| 15:2: |      ![]. ].](_drbrack.gif)  
       ![]. ].](_drbrack.gif)  
    ![]. ].](_drbrack.gif)  
| 16:15,14: |      ![]. ].](_drbrack.gif)  
        
 
| 17:2: |     ![]_ ]_](_urbrack.gif)  
    ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif) 
| 18:2: |     ![]_ ]_](_urbrack.gif)  
| 19:2: |     ![]_ ]_](_urbrack.gif)
| 20:18,19: |      ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)     
| 21:17,20: |     ![]_ ]_](_urbrack.gif)   
 
| 22:2: |      ![]. ].](_drbrack.gif)  
    ![]_ ]_](_urbrack.gif)      

| 23:2: |     ![]_ ]_](_urbrack.gif)
| 24:21,23: |      ![]_ ]_](_urbrack.gif)  
    ![]_ ]_](_urbrack.gif)     
| 25:22,24: |      ![]. ].](_drbrack.gif)  
    
| 26:2: |      ![]. ].](_drbrack.gif)
  
| 27:25,26: |       ![]. ].](_drbrack.gif)
   ![]. ].](_drbrack.gif)       
   
| 28:2: |      ![]. ].](_drbrack.gif)  
       ![]. ].](_drbrack.gif)   
 ![]. ].](_drbrack.gif)    
| 29:27,28: |      ![]. ].](_drbrack.gif)  
        
   | |