Type  Label  Description 
Statement 

Theorem  uunT11p2 37101 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uunT12 37102 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uunT12p1 37103 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uunT12p2 37104 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uunT12p3 37105 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uunT12p4 37106 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uunT12p5 37107 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uun111 37108 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  3anidm12p1 37109 
A deduction unionizing a nonunionized collection of virtual hypotheses.
3anidm12 1321 denotes the deduction which would have been
named uun112 if
it did not preexist in set.mm. This second permutation's name is based
on this preexisting name. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  3anidm12p2 37110 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uun123 37111 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uun123p1 37112 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uun123p2 37113 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uun123p3 37114 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uun123p4 37115 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uun2221 37116 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 30Dec2016.)
(Proof modification is discouraged.) (New usage is discouraged.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uun2221p1 37117 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  uun2221p2 37118 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  3impdirp1 37119 
A deduction unionizing a nonunionized collection of virtual
hypotheses. Commuted version of 3impdir 1320. (Contributed by Alan Sare,
4Feb2017.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  3impcombi 37120 
A 1hypothesis propositional calculus deduction. (Contributed by Alan
Sare, 25Sep2017.)



Theorem  3imp231 37121 
Importation inference. (Contributed by Alan Sare, 17Oct2017.)



21.29.6 Theorems proved using Virtual
Deduction


Theorem  trsspwALT 37122 
Virtual deduction proof of the lefttoright implication of dftr4 4461. A
transitive class is a subset of its power class. This proof corresponds
to the virtual deduction proof of dftr4 4461 without accumulating results.
(Contributed by Alan Sare, 29Apr2011.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  trsspwALT2 37123 
Virtual deduction proof of trsspwALT 37122. This proof is the same as the
proof of trsspwALT 37122 except each virtual deduction symbol is
replaced by
its nonvirtual deduction symbol equivalent. A transitive class is a
subset of its power class. (Contributed by Alan Sare, 23Jul2011.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  trsspwALT3 37124 
Short predicate calculus proof of the lefttoright implication of
dftr4 4461. 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 37123, which is the virtual deduction proof trsspwALT 37122
without virtual deductions. (Contributed by Alan Sare, 30Apr2011.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  sspwtr 37125 
Virtual deduction proof of the righttoleft implication of dftr4 4461. A
class which is a subclass of its power class is transitive. This proof
corresponds to the virtual deduction proof of sspwtr 37125 without
accumulating results. (Contributed by Alan Sare, 2May2011.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  sspwtrALT 37126 
Virtual deduction proof of sspwtr 37125. This proof is the same as the
proof of sspwtr 37125 except each virtual deduction symbol is
replaced by
its nonvirtual deduction symbol equivalent. A class which is a
subclass of its power class is transitive. (Contributed by Alan Sare,
3May2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  csbabgOLD 37127* 
Move substitution into a class abstraction. (Contributed by NM,
13Dec2005.) (Proof shortened by Andrew Salmon, 9Jul2011.) Obsolete
as of 19Aug2018. Use csbab 3765 instead. (New usage is discouraged.)
(Proof modification is discouraged.)



Theorem  csbunigOLD 37128 
Distribute proper substitution through the union of a class.
(Contributed by Alan Sare, 10Nov2012.) Obsolete as of 22Aug2018.
Use csbuni 4185 instead. (New usage is discouraged.)
(Proof modification is discouraged.)



Theorem  csbfv12gALTOLD 37129 
Move class substitution in and out of a function value. The proof is
derived from the virtual deduction proof csbfv12gALTVD 37212. (Contributed
by Alan Sare, 10Nov2012.) Obsolete as of 20Aug2018. Use csbfv12 5855
instead. (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  csbxpgOLD 37130 
Distribute proper substitution through the Cartesian product of two
classes. (Contributed by Alan Sare, 10Nov2012.) Obsolete as of
23Aug2018. Use csbrn 5254 instead. (New usage is discouraged.)
(Proof modification is discouraged.)



Theorem  csbingOLD 37131 
Distribute proper substitution through an intersection relation.
(Contributed by Alan Sare, 22Jul2012.) Obsolete as of 18Aug2018.
Use csbin 3767 instead. (New usage is discouraged.)
(Proof modification is discouraged.)



Theorem  csbresgOLD 37132 
Distribute proper substitution through the restriction of a class.
csbresgOLD 37132 is derived from the virtual deduction proof
csbresgVD 37208.
(Contributed by Alan Sare, 10Nov2012.) Obsolete as of 23Aug2018. Use
csbres 5065 instead. (New usage is discouraged.)
(Proof modification is discouraged.)



Theorem  csbrngOLD 37133 
Distribute proper substitution through the range of a class.
(Contributed by Alan Sare, 10Nov2012.) Obsolete as of 23Aug2018.
Use csbrn 5254 instead. (New usage is discouraged.)
(Proof modification is discouraged.)



Theorem  csbima12gALTOLD 37134 
Move class substitution in and out of the image of a function. The proof
is derived from the virtual deduction proof csbima12gALTVD 37210.
(Contributed by Alan Sare, 10Nov2012.) Obsolete as of 20Aug2018. Use
csbfv12 5855 instead. (Proof modification is
discouraged.) (Proof
modification is discouraged.) (New usage is discouraged.)



Theorem  sspwtrALT2 37135 
Short predicate calculus proof of the righttoleft implication of
dftr4 4461. 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 37126, which is the virtual deduction
proof sspwtr 37125 without virtual deductions. (Contributed by
Alan Sare,
3May2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  pwtrVD 37136 
Virtual deduction proof of pwtr 4612; see pwtrrVD 37137 for the converse.
(Contributed by Alan Sare, 25Aug2011.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  pwtrrVD 37137 
Virtual deduction proof of pwtr 4612; see pwtrVD 37136 for the converse.
(Contributed by Alan Sare, 25Aug2011.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  suctrALT 37138 
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 37138 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 5463 for the original proof.
(Contributed by Alan Sare, 11Apr2009.) (Revised by Alan Sare,
12Jun2018.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  snssiALTVD 37139 
Virtual deduction proof of snssiALT 37140. (Contributed by Alan Sare,
11Sep2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  snssiALT 37140 
If a class is an element of another class, then its singleton is a
subclass of that other class. Alternate proof of snssi 4082. This
theorem was automatically generated from snssiALTVD 37139 using a
translation program. (Contributed by Alan Sare, 11Sep2011.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  snsslVD 37141 
Virtual deduction proof of snssl 37142. (Contributed by Alan Sare,
25Aug2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  snssl 37142 
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
righttoleft implication of the biconditional snss 4062.
The proof of
this theorem was automatically generated from snsslVD 37141 using a tools
command file, translateMWO.cmd, by translating the proof into its
nonvirtual deduction form and minimizing it. (Contributed by Alan
Sare, 25Aug2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  snelpwrVD 37143 
Virtual deduction proof of snelpwi 4604. (Contributed by Alan Sare,
25Aug2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  unipwrVD 37144 
Virtual deduction proof of unipwr 37145. (Contributed by Alan Sare,
25Aug2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  unipwr 37145 
A class is a subclass of the union of its power class. This theorem is
the righttoleft subclass lemma of unipw 4609. The proof of this theorem
was automatically generated from unipwrVD 37144 using a tools command file ,
translateMWO.cmd , by translating the proof into its nonvirtual
deduction form and minimizing it. (Contributed by Alan Sare,
25Aug2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  sstrALT2VD 37146 
Virtual deduction proof of sstrALT2 37147. (Contributed by Alan Sare,
11Sep2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  sstrALT2 37147 
Virtual deduction proof of sstr 3410, transitivity of subclasses, Theorem
6 of [Suppes] p. 23. This theorem was
automatically generated from
sstrALT2VD 37146 using the command file translate_{without}_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, 11Sep2011.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  suctrALT2VD 37148 
Virtual deduction proof of suctrALT2 37149. (Contributed by Alan Sare,
11Sep2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  suctrALT2 37149 
Virtual deduction proof of suctr 5463. The sucessor of a transitive class
is transitive. This proof was generated automatically from the virtual
deduction proof suctrALT2VD 37148 using the tools command file
translate_{without}_overwriting_{minimize}_excluding_{duplicates}.cmd .
(Contributed by Alan Sare, 11Sep2011.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  elex2VD 37150* 
Virtual deduction proof of elex2 3029. (Contributed by Alan Sare,
25Sep2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  elex22VD 37151* 
Virtual deduction proof of elex22 3030. (Contributed by Alan Sare,
24Oct2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  eqsbc3rVD 37152* 
Virtual deduction proof of eqsbc3r 3294. (Contributed by Alan Sare,
24Oct2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  zfregs2VD 37153* 
Virtual deduction proof of zfregs2 8164. (Contributed by Alan Sare,
24Oct2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  tpid3gVD 37154 
Virtual deduction proof of tpid3g 4053. (Contributed by Alan Sare,
24Oct2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  en3lplem1VD 37155* 
Virtual deduction proof of en3lplem1 8067. (Contributed by Alan Sare,
24Oct2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  en3lplem2VD 37156* 
Virtual deduction proof of en3lplem2 8068. (Contributed by Alan Sare,
24Oct2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  en3lpVD 37157 
Virtual deduction proof of en3lp 8069. (Contributed by Alan Sare,
24Oct2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



21.29.7 Theorems proved using Virtual Deduction
with mmj2 assistance


Theorem  simplbi2VD 37158 
Virtual deduction proof of simplbi2 629. 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 37075 
 qed:3,?: e0a 37075 

The proof of simplbi2 629 was automatically derived from it.
(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  3ornot23VD 37159 
Virtual deduction proof of 3ornot23 36778. 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 36920 
 4:1,?: e1a 36920 
 5:3,4,?: e11 36981 
 6:2,?: e2 36924 
 7:5,6,?: e12 37027 
 8:7: 
 qed:8: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  orbi1rVD 37160 
Virtual deduction proof of orbi1r 36779. 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 36924 
 4:1,3,?: e12 37027 
 5:4,?: e2 36924 
 6:5: 
 7:: 
 8:7,?: e2 36924 
 9:1,8,?: e12 37027 
 10:9,?: e2 36924 
 11:10: 
 12:6,11,?: e11 36981 
 qed:12: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  bitr3VD 37161 
Virtual deduction proof of bitr3 36780. 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 36920 
 3:: 
 4:3,?: e2 36924 
 5:2,4,?: e12 37027 
 6:5: 
 qed:6: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  3orbi123VD 37162 
Virtual deduction proof of 3orbi123 36781. 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 36920 
 3:1,?: e1a 36920 
 4:1,?: e1a 36920 
 5:2,3,?: e11 36981 
 6:5,4,?: e11 36981 
 7:?: 
 8:6,7,?: e10 36987 
 9:?: 
 10:8,9,?: e10 36987 
 qed:10: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sbc3orgVD 37163 
Virtual deduction proof of sbc3orgOLD 36806. 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 36920 
 3:: 
 32:3: 
 33:1,32,?: e10 36987 
 4:1,33,?: e11 36981 
 5:2,4,?: e11 36981 
 6:1,?: e1a 36920 
 7:6,?: e1a 36920 
 8:5,7,?: e11 36981 
 9:?: 
 10:8,9,?: e10 36987 
 qed:10: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  19.21a3con13vVD 37164* 
Virtual deduction proof of alrim3con13v 36807. 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 36924 
 4:2,?: e2 36924 
 5:2,?: e2 36924 
 6:1,4,?: e12 37027 
 7:3,?: e2 36924 
 8:5,?: e2 36924 
 9:7,6,8,?: e222 36929 
 10:9,?: e2 36924 
 11:10:in2 
 qed:11:in1 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  exbirVD 37165 
Virtual deduction proof of exbir 36746. 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 37027 
 6:3,5,?: e32 37061 
 7:6: 
 8:7: 
 9:8,?: e1a 36920 
 qed:9: 

(Contributed by Alan Sare, 13Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  exbiriVD 37166 
Virtual deduction proof of exbiri 626. 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 36987 
 6:3,5,?: e21 37033 
 7:4,6,?: e32 37061 
 8:7: 
 9:8: 
 qed:9: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  rspsbc2VD 37167* 
Virtual deduction proof of rspsbc2 36808. 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 37051 
 5:1,4,?: e13 37051 
 6:2,5,?: e23 37058 
 7:6: 
 8:7: 
 qed:8: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  3impexpVD 37168 
Virtual deduction proof of 3impexp 1227. 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 36987 
 4:3,?: e1a 36920 
 5:4,?: e1a 36920 
 6:5: 
 7:: 
 8:7,?: e1a 36920 
 9:8,?: e1a 36920 
 10:2,9,?: e01 36984 
 11:10: 
 qed:6,11,?: e00 37071 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  3impexpbicomVD 37169 
Virtual deduction proof of 3impexpbicom 36747. 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 36987 
 4:3,?: e1a 36920 
 5:4: 
 6:: 
 7:6,?: e1a 36920 
 8:7,2,?: e10 36987 
 9:8: 
 qed:5,9,?: e00 37071 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  3impexpbicomiVD 37170 
Virtual deduction proof of 3impexpbicomi 36748. 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, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sbcel1gvOLD 37171* 
Class substitution into a membership relation. (Contributed by NM,
17Nov2006.) (Proof shortened by Andrew Salmon, 29Jun2011.)
Obsolete as of 17Aug2018. Use sbcel1v 3296 instead.
(New usage is discouraged.) (Proof modification is discouraged.)



Theorem  sbcoreleleqVD 37172* 
Virtual deduction proof of sbcoreleleq 36809. 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 36920 
 3:1,?: e1a 36920 
 4:1,?: e1a 36920 
 5:2,3,4,?: e111 36967 
 6:1,?: e1a 36920 
 7:5,6: e11 36981 
 qed:7: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  hbra2VD 37173* 
Virtual deduction proof of nfra2 2747. 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 37071 
 4:2: 
 5:4,?: e0a 37075 
 qed:3,5,?: e00 37071 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  tratrbVD 37174* 
Virtual deduction proof of tratrb 36810. 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 36920 
 3:1,?: e1a 36920 
 4:1,?: e1a 36920 
 5:: 
 6:5,?: e2 36924 
 7:5,?: e2 36924 
 8:2,7,4,?: e121 36949 
 9:2,6,8,?: e122 36946 
 10:: 
 11:6,7,10,?: e223 36928 
 12:11: 
 13:: 
 14:12,13,?: e20 37030 
 15:: 
 16:7,15,?: e23 37058 
 17:6,16,?: e23 37058 
 18:17: 
 19:: 
 20:18,19,?: e20 37030 
 21:3,?: e1a 36920 
 22:21,9,4,?: e121 36949 
 23:22,?: e2 36924 
 24:4,23,?: e12 37027 
 25:14,20,24,?: e222 36929 
 26:25: 
 27:: 
 28:27,?: e0a 37075 
 29:28,26: 
 30:: 
 31:30,?: e0a 37075 
 32:31,29: 
 33:32,?: e1a 36920 
 qed:33: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  al2imVD 37175 
Virtual deduction proof of al2im 1680. 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 36920 
 3:: 
 4:2,3,?: e10 36987 
 qed:4: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  syl5impVD 37176 
Virtual deduction proof of syl5imp 36782. 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 36920 
 3:: 
 4:3,2,?: e21 37033 
 5:4,?: e2 36924 
 6:5: 
 qed:6: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  idiVD 37177 
Virtual deduction proof of idiALT 36745. 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, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  ancomstVD 37178 
Closed form of ancoms 454. 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 453 is derived automatically from it.
(Contributed by Alan Sare, 25Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  ssralv2VD 37179* 
Quantification restricted to a subclass for two quantifiers. ssralv 3463
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 36801 is ssralv2VD 37179 without
virtual deductions and was automatically derived from ssralv2VD 37179.
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, 10Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  ordelordALTVD 37180 
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36. This is an alternate proof of ordelord 5402 using
the Axiom of Regularity indirectly through dford2 8073. 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 36811 is ordelordALTVD 37180
without virtual deductions and was automatically derived from
ordelordALTVD 37180 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, 12Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  equncomVD 37181 
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 3549 is equncomVD 37181 without
virtual deductions and was automatically derived from equncomVD 37181.
1:: 
 2:: 
 3:1,2: 
 4:3: 
 5:: 
 6:5,2: 
 7:6: 
 8:4,7: 

(Contributed by Alan Sare, 17Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  equncomiVD 37182 
Inference form of equncom 3549. 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 3550 is equncomiVD 37182 without
virtual deductions and was automatically derived from equncomiVD 37182.
(Contributed by Alan Sare, 18Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sucidALTVD 37183 
A set belongs to its successor. Alternate proof of sucid 5459.
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 37184 is sucidALTVD 37183
without virtual deductions and was automatically derived from
sucidALTVD 37183. 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 0virtual 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 dfsuc 5386, 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 8073.
h1:: 
 2:1: 
 3:2: 
 4:: 
 qed:3,4: 

(Contributed by Alan Sare, 18Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sucidALT 37184 
A set belongs to its successor. This proof was automatically derived
from sucidALTVD 37183 using translate_{without}_overwriting.cmd and
minimizing. (Contributed by Alan Sare, 18Feb2012.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  sucidVD 37185 
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 5459 is sucidVD 37185 without virtual deductions and was automatically
derived from sucidVD 37185.
h1:: 
 2:1: 
 3:2: 
 4:: 
 qed:3,4: 

(Contributed by Alan Sare, 18Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  imbi12VD 37186 
Implication form of imbi12i 327.
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 323 is imbi12VD 37186 without virtual deductions and was automatically
derived from imbi12VD 37186.
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, 18Mar2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  imbi13VD 37187 
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 36790 is imbi13VD 37187 without virtual deductions and was automatically
derived from imbi13VD 37187.
1:: 
 2:: 
 3:: 
 4:2,3: 
 5:1,4: 
 6:5: 
 7:6: 
 qed:7: 

(Contributed by Alan Sare, 18Mar2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sbcim2gVD 37188 
Distribution of class substitution over a leftnested implication.
Similar to sbcimg 3279.
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 36812 is sbcim2gVD 37188 without virtual deductions and was automatically
derived from sbcim2gVD 37188.
1:: 
 2:: 
 3:1,2: 
 4:1: 
 5:3,4: 
 6:5: 
 7:: 
 8:4,7: 
 9:1: 
 10:8,9: 
 11:10: 
 12:6,11: 
 qed:12: 

(Contributed by Alan Sare, 18Mar2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sbcbiVD 37189 
Implication form of sbcbiiOLD 36805.
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 36813 is sbcbiVD 37189 without virtual deductions and was automatically
derived from sbcbiVD 37189.
1:: 
 2:: 
 3:1,2: 
 4:1,3: 
 5:4: 
 qed:5: 

(Contributed by Alan Sare, 18Mar2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  trsbcVD 37190* 
Formulabuilding 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 36814 is trsbcVD 37190 without virtual deductions and was automatically
derived from trsbcVD 37190.
1:: 
 2:1: 
 3:1: 
 4:1: 
 5:1,2,3,4: 
 6:1: 
 7:5,6: 
 8:: 
 9:7,8: 
 10:: 
 11:10: 
 12:1,11: 
 13:9,12: 
 14:13: 
 15:14: 
 16:1: 
 17:15,16: 
 18:17: 
 19:18: 
 20:1: 
 21:19,20: 
 22:: 
 23:21,22: 
 24:: 
 25:24: 
 26:1,25: 
 27:23,26: 
 qed:27: 

(Contributed by Alan Sare, 18Mar2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  truniALTVD 37191* 
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 36815 is truniALTVD 37191 without virtual deductions and was
automatically derived from truniALTVD 37191.
1:: 
 2:: 
 3:2: 
 4:2: 
 5:4: 
 6:: 
 7:6: 
 8:6: 
 9:1,8: 
 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, 18Mar2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  ee33VD 37192 
Nonvirtual deduction form of e33 37037.
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 36791 is ee33VD 37192 without virtual deductions and was automatically
derived from ee33VD 37192.
h1:: 
 h2:: 
 h3:: 
 4:1,3: 
 5:4: 
 6:2,5: 
 7:6: 
 8:7: 
 qed:8: 

(Contributed by Alan Sare, 18Mar2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  trintALTVD 37193* 
The intersection of a class of transitive sets is transitive. Virtual
deduction proof of trintALT 37194.
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 37194 is trintALTVD 37193 without virtual deductions and was
automatically derived from trintALTVD 37193.
1:: 
 2:: 
 3:2: 
 4:2: 
 5:4: 
 6:5: 
 7:: 
 8:7,6: 
 9:7,1: 
 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, 17Apr2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  trintALT 37194* 
The intersection of a class of transitive sets is transitive. Exercise
5(b) of [Enderton] p. 73. trintALT 37194 is an alternate proof of trint 4471.
trintALT 37194 is trintALTVD 37193 without virtual deductions and was
automatically derived from trintALTVD 37193 using the tools program
translate..without..overwriting.cmd and Metamath's minimize command.
(Contributed by Alan Sare, 17Apr2012.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  undif3VD 37195 
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 37195 without virtual deductions and was automatically
derived from undif3VD 37195.
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, 17Apr2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sbcssgVD 37196 
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 37196 without virtual deductions and was automatically
derived from sbcssgVD 37196.
1:: 
 2:1: 
 3:1: 
 4:2,3: 
 5:1: 
 6:4,5: 
 7:6: 
 8:7: 
 9:1: 
 10:8,9: 
 11:: 
 110:11: 
 12:1,110: 
 13:10,12: 
 14:: 
 15:13,14: 
 qed:15: 

(Contributed by Alan Sare, 22Jul2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  csbingVD 37197 
Virtual deduction proof of csbingOLD 37131.
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 37131 is csbingVD 37197 without virtual deductions and was
automatically derived from csbingVD 37197.
1:: 
 2:: 
 20:2: 
 30:1,20: 
 3:1,30: 
 4:1: 
 5:3,4: 
 6:1: 
 7:1: 
 8:6,7: 
 9:1: 
 10:9,8: 
 11:10: 
 12:11: 
 13:5,12: 
 14:: 
 15:13,14: 
 qed:15: 

(Contributed by Alan Sare, 22Jul2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  onfrALTlem5VD 37198* 
Virtual deduction proof of onfrALTlem5 36821.
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 36821 is onfrALTlem5VD 37198 without virtual deductions and was
automatically derived from onfrALTlem5VD 37198.
1:: 
 2:1: 
 3:2: 
 4:3: 
 5:: 
 6:4,5: 
 7:2: 
 8:: 
 9:8: 
 10:2,9: 
 11:7,10: 
 12:6,11:   