Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  3anidm12p1 27714 
A deduction unionizing a nonunionized collection of virtual hypotheses.
3anidm12 1244 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 27715 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



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



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



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



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



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



Theorem  uun2221 27721 
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 27722 
A deduction unionizing a nonunionized collection of virtual
hypotheses. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



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



Theorem  3impdirp1 27724 
A deduction unionizing a nonunionized collection of virtual hypotheses.
3impdir 1243 is ~? uun3132 and is in set.mm. 3impdirp1 27724 is ~?
uun3132p1. (Contributed by Alan Sare, 4Feb2017.)
(Proof modification is discouraged.) (New usage is discouraged.)



18.23.4 Theorems proved using virtual
deduction


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



Theorem  trsspwALT2 27726 
Virtual deduction proof of trsspwALT 27725. This proof is the same as the
proof of trsspwALT 27725 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 27727 
Short predicate calculus proof of the lefttoright implication of
dftr4 4092. 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 27726, which is the virtual deduction proof trsspwALT 27725
without virtual deductions. (Contributed by Alan Sare, 30Apr2011.)
(Proof modification is discouraged.) (New usage is discouraged.)



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



Theorem  sspwtrALT 27729 
Virtual deduction proof of sspwtr 27728. This proof is the same as the
proof of sspwtr 27728 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  sspwtrALT2 27730 
Short predicate calculus proof of the righttoleft implication of
dftr4 4092. 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 27729, which is the virtual deduction
proof sspwtr 27728 without virtual deductions. (Contributed by
Alan Sare,
3May2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  pwtrVD 27731 
Virtual deduction proof of pwtrOLD 27732. (Contributed by Alan Sare,
25Aug2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  pwtrOLD 27732 
The power class of a transitive class is transitive. The proof of this
theorem was automatically generated from pwtrVD 27731 using a tools command
file, translateMWO.cmd , by translating the proof into its nonvirtual
deduction form and minimizing it. (Contributed by Alan Sare,
25Aug2011.) (Moved into main set.mm as pwtr 4198
and may be deleted by
mathbox owner, AS. NM 15Jun2014.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  pwtrrVD 27733 
Virtual deduction proof of pwtrrOLD 27734. (Contributed by Alan Sare,
25Aug2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  pwtrrOLD 27734 
A set is transitive if its power set is. The proof of this theorem was
automatically generated from pwtrrVD 27733 using a tools command file,
translateMWO.cmd , by translating the proof into its nonvirtual
deduction form and minimizing it. (Contributed by Alan Sare,
25Aug2011.) (Moved into main set.mm as pwtr 4198
and may be deleted by
mathbox owner, AS. NM 15Jun2014.)
(Proof modification is discouraged.) (New usage is discouraged.)



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



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



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



Theorem  snssl 27738 
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 3722.
The proof of
this theorem was automatically generated from snsslVD 27737 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 27739 
Virtual deduction proof of snelpwi 4192. (Contributed by Alan Sare,
25Aug2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  snelpwrOLD 27740 
If a class is contained in another class, then its singleton is
contained in the power class of that other class. This theorem is the
lefttoright implication of the biconditional snelpw 4193. Unlike
snelpw 4193, may be a proper class. The proof of this theorem was
automatically generated from snelpwrVD 27739 using a tools command file,
translateMWO.cmd , by translating the proof into its nonvirtual
deduction form and minimizing it. (Moved to snelpwi 4192 in main set.mm
and may be deleted by mathbox owner, AS. NM 10Sep2013.)
(Contributed by Alan Sare, 25Aug2011.)
(Proof modification is discouraged.) (New usage is discouraged.)



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



Theorem  unipwr 27742 
A class is a subclass of the union of its power class. This theorem is
the righttoleft subclass lemma of unipw 4196. The proof of this theorem
was automatically generated from unipwrVD 27741 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 27743 
Virtual deduction proof of sstrALT2 27744. (Contributed by Alan Sare,
11Sep2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  sstrALT2 27744 
Virtual deduction proof of sstr 3162, transitivity of subclasses, Theorem
6 of [Suppes] p. 23. This theorem was
automatically generated from
sstrALT2VD 27743 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 27745 
Virtual deduction proof of suctrALT2 27746. (Contributed by Alan Sare,
11Sep2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  suctrALT2 27746 
Virtual deduction proof of suctr 4447. The sucessor of a transitive class
is transitive. This proof was generated automatically from the virtual
deduction proof suctrALT2VD 27745 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 27747* 
Virtual deduction proof of elex2 2775. (Contributed by Alan Sare,
25Sep2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



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



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



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



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



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



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



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



18.23.5 Theorems proved using virtual deduction
with mmj2 assistance


Theorem  simplbi2VD 27755 
Virtual deduction proof of simplbi2 611. 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,?: e0_ 27680 
 qed:3,?: e0_ 27680 

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



Theorem  3ornot23VD 27756 
Virtual deduction proof of 3ornot23 27406. 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,?: e1_ 27532 
 4:1,?: e1_ 27532 
 5:3,4,?: e11 27593 
 6:2,?: e2 27536 
 7:5,6,?: e12 27632 
 8:7: 
 qed:8: 

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



Theorem  orbi1rVD 27757 
Virtual deduction proof of orbi1r 27407. 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 27536 
 4:1,3,?: e12 27632 
 5:4,?: e2 27536 
 6:5: 
 7:: 
 8:7,?: e2 27536 
 9:1,8,?: e12 27632 
 10:9,?: e2 27536 
 11:10: 
 12:6,11,?: e11 27593 
 qed:12: 

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



Theorem  bitr3VD 27758 
Virtual deduction proof of bitr3 27408. 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,?: e1_ 27532 
 3:: 
 4:3,?: e2 27536 
 5:2,4,?: e12 27632 
 6:5: 
 qed:6: 

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



Theorem  3orbi123VD 27759 
Virtual deduction proof of 3orbi123 27409. 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,?: e1_ 27532 
 3:1,?: e1_ 27532 
 4:1,?: e1_ 27532 
 5:2,3,?: e11 27593 
 6:5,4,?: e11 27593 
 7:?: 
 8:6,7,?: e10 27600 
 9:?: 
 10:8,9,?: e10 27600 
 qed:10: 

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



Theorem  sbc3orgVD 27760 
Virtual deduction proof of sbc3org 27431. 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,?: e1_ 27532 
 3:: 
 32:3: 
 33:1,32,?: e10 27600 
 4:1,33,?: e11 27593 
 5:2,4,?: e11 27593 
 6:1,?: e1_ 27532 
 7:6,?: e1_ 27532 
 8:5,7,?: e11 27593 
 9:?: 
 10:8,9,?: e10 27600 
 qed:10: 

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



Theorem  19.21a3con13vVD 27761* 
Virtual deduction proof of alrim3con13v 27432. 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 27536 
 4:2,?: e2 27536 
 5:2,?: e2 27536 
 6:1,4,?: e12 27632 
 7:3,?: e2 27536 
 8:5,?: e2 27536 
 9:7,6,8,?: e222 27541 
 10:9,?: e2 27536 
 11:10:in2 
 qed:11:in1 

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



Theorem  exbirVD 27762 
Virtual deduction proof of exbir 1361. 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 27632 
 6:3,5,?: e32 27666 
 7:6: 
 8:7: 
 9:8,?: e1_ 27532 
 qed:9: 

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



Theorem  exbiriVD 27763 
Virtual deduction proof of exbiri 608. 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 27600 
 6:3,5,?: e21 27638 
 7:4,6,?: e32 27666 
 8:7: 
 9:8: 
 qed:9: 

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



Theorem  ra4sbc2VD 27764* 
Virtual deduction proof of ra4sbc2 27433. 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 27656 
 5:1,4,?: e13 27656 
 6:2,5,?: e23 27663 
 7:6: 
 8:7: 
 qed:8: 

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



Theorem  3impexpVD 27765 
Virtual deduction proof of 3impexp 1362. 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 27600 
 4:3,?: e1_ 27532 
 5:4,?: e1_ 27532 
 6:5: 
 7:: 
 8:7,?: e1_ 27532 
 9:8,?: e1_ 27532 
 10:2,9,?: e01 27596 
 11:10: 
 qed:6,11,?: e00 27676 

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



Theorem  3impexpbicomVD 27766 
Virtual deduction proof of 3impexpbicom 1363. 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 27600 
 4:3,?: e1_ 27532 
 5:4: 
 6:: 
 7:6,?: e1_ 27532 
 8:7,2,?: e10 27600 
 9:8: 
 qed:5,9,?: e00 27676 

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



Theorem  3impexpbicomiVD 27767 
Virtual deduction proof of 3impexpbicomi 1364. 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  sbcoreleleqVD 27768* 
Virtual deduction proof of sbcoreleleq 27434. 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,?: e1_ 27532 
 3:1,?: e1_ 27532 
 4:1,?: e1_ 27532 
 5:2,3,4,?: e111 27579 
 6:1,?: e1_ 27532 
 7:5,6: e11 27593 
 qed:7: 

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



Theorem  hbra2VD 27769* 
Virtual deduction proof of nfra2 2572. 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 27676 
 4:2: 
 5:4,?: e0_ 27680 
 qed:3,5,?: e00 27676 

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



Theorem  tratrbVD 27770* 
Virtual deduction proof of tratrb 27435. 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,?: e1_ 27532 
 3:1,?: e1_ 27532 
 4:1,?: e1_ 27532 
 5:: 
 6:5,?: e2 27536 
 7:5,?: e2 27536 
 8:2,7,4,?: e121 27561 
 9:2,6,8,?: e122 27558 
 10:: 
 11:6,7,10,?: e223 27540 
 12:11: 
 13:: 
 14:12,13,?: e20 27635 
 15:: 
 16:7,15,?: e23 27663 
 17:6,16,?: e23 27663 
 18:17: 
 19:: 
 20:18,19,?: e20 27635 
 21:3,?: e1_ 27532 
 22:21,9,4,?: e121 27561 
 23:22,?: e2 27536 
 24:4,23,?: e12 27632 
 25:14,20,24,?: e222 27541 
 26:25: 
 27:: 
 28:27,?: e0_ 27680 
 29:28,26: 
 30:: 
 31:30,?: e0_ 27680 
 32:31,29: 
 33:32,?: e1_ 27532 
 qed:33: 

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



Theorem  3ax5VD 27771 
Virtual deduction proof of 3ax5 27436. 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,?: e1_ 27532 
 3:: 
 4:2,3,?: e10 27600 
 qed:4: 

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



Theorem  syl5impVD 27772 
Virtual deduction proof of syl5imp 27410. 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,?: e1_ 27532 
 3:: 
 4:3,2,?: e21 27638 
 5:4,?: e2 27536 
 6:5: 
 qed:6: 

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



Theorem  idiVD 27773 
Virtual deduction proof of idi 2. 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  ancomsimpVD 27774 
Closed form of ancoms 441. 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, 25Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  ssralv2VD 27775* 
Quantification restricted to a subclass for two quantifiers. ssralv 3212
for two quantifiers. The following User's Proof is a Virtual Deduction
proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. ssralv2 27430 is ssralv2VD 27775 without
virtual deductions and was automatically derived from ssralv2VD 27775.
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 27776 
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36. This is an alternate proof of ordelord 4386 using
the Axiom of Regularity indirectly through dford2 7289. 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 O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. ordelordALT 27437 is ordelordALTVD 27776
without virtual deductions and was automatically derived from
ordelordALTVD 27776 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 27777 
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 O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. equncom 3295 is equncomVD 27777 without
virtual deductions and was automatically derived from equncomVD 27777.
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 27778 
Inference form of equncom 3295. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. equncomi 3296 is equncomiVD 27778 without
virtual deductions and was automatically derived from equncomiVD 27778.
(Contributed by Alan Sare, 18Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sucidALTVD 27779 
A set belongs to its successor. Alternate proof of sucid 4443.
The following User's Proof is a Virtual Deduction proof
completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. sucidALT 27780 is sucidALTVD 27779
without virtual deductions and was automatically derived from
sucidALTVD 27779. 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 4370, a
reference definition (axiom) in set.mm. Also, a theorem or
deduction is said to be a semantic variation of a 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 7289.
h1:: 
 2:1: 
 3:2: 
 4:: 
 qed:3,4: 

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



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



Theorem  sucidVD 27781 
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 O'Cat's mmj2
and Norm Megill's Metamath Proof Assistant. sucid 4443 is
sucidVD 27781 without virtual deductions and was automatically
derived from sucidVD 27781.
h1:: 
 2:1: 
 3:2: 
 4:: 
 qed:3,4: 

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



Theorem  imbi12VD 27782 
Implication form of imbi12i 318. The following User's Proof is a Virtual
Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi12 27418
is imbi12VD 27782 without virtual deductions and was automatically derived
from imbi12VD 27782.
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 27783 
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 O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi13 27419
is imbi13VD 27783 without virtual deductions and was automatically derived
from imbi13VD 27783.
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 27784 
Distribution of class substitution over a leftnested implication.
Similar
to sbcimg 3007. The following User's Proof is a Virtual Deduction proof
completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcim2g 27438
is sbcim2gVD 27784 without virtual deductions and was automatically derived
from sbcim2gVD 27784.
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 27785 
Implication form of sbcbiiOLD 3022. The following User's Proof is a
Virtual
Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcbi 27439
is sbcbiVD 27785 without virtual deductions and was automatically derived
from sbcbiVD 27785.
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 27786* 
Formulabuilding inference rule for class substitution, substituting a
class
variable for the set 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 O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trsbc 27440
is trsbcVD 27786 without virtual deductions and was automatically derived
from trsbcVD 27786.
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 27787* 
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 O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. truniALT 27441
is truniALTVD 27787 without virtual deductions and was automatically derived
from truniALTVD 27787.
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 27788 
Nonvirtual deduction form of e33 27642. The following User's Proof is a
Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. ee33 27420
is ee33VD 27788 without virtual deductions and was automatically derived
from ee33VD 27788.
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 27789* 
The intersection of a class of transitive sets is transitive. Virtual
deduction proof of trintALT 27790.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trintALT 27790
is trintALTVD 27789 without virtual deductions and was automatically derived
from trintALTVD 27789.
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 27790* 
The intersection of a class of transitive sets is transitive. Exercise
5(b) of [Enderton] p. 73. trintALT 27790 is an alternative proof of
trint 4102. trintALT 27790 is trintALTVD 27789 without virtual deductions and was
automatically derived from trintALTVD 27789 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 27791 
The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual
deduction proof of undif3 3404.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. undif3 3404
is undif3VD 27791 without virtual deductions and was automatically derived
from undif3VD 27791.
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  sbcssVD 27792 
Virtual deduction proof of sbcss 27442.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcss 27442
is sbcssVD 27792 without virtual deductions and was automatically derived
from sbcssVD 27792.
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 27793 
Virtual deduction proof of csbing 3351.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbing 3351
is csbingVD 27793 without virtual deductions and was automatically derived
from csbingVD 27793.
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 27794* 
Virtual deduction proof of onfrALTlem5 27443.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
onfrALTlem5 27443 is onfrALTlem5VD 27794 without virtual deductions and was
automatically derived
from onfrALTlem5VD 27794.
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: 
 13:2: 
 14:12,13: 
 15:2: 
 