Type  Label  Description 
Statement 

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



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



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



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



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



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



18.25.6 Theorems proved using virtual
deduction


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



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



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



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



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



Theorem  pwtrOLD 28915 
The power class of a transitive class is transitive. The proof of this
theorem was automatically generated from pwtrVD 28914 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 4242
and may be deleted by
mathbox owner, AS. NM 15Jun2014.)
(Proof modification is discouraged.) (New usage is discouraged.)



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



Theorem  pwtrrOLD 28917 
A set is transitive if its power set is. The proof of this theorem was
automatically generated from pwtrrVD 28916 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 4242
and may be deleted by
mathbox owner, AS. NM 15Jun2014.)
(Proof modification is discouraged.) (New usage is discouraged.)



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



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



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



Theorem  snssl 28921 
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 3761.
The proof of
this theorem was automatically generated from snsslVD 28920 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 28922 
Virtual deduction proof of snelpwi 4236. (Contributed by Alan Sare,
25Aug2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  snelpwrOLD 28923 
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 4237. Unlike
snelpw 4237, may be a proper class. The proof of this theorem was
automatically generated from snelpwrVD 28922 using a tools command file,
translateMWO.cmd , by translating the proof into its nonvirtual
deduction form and minimizing it. (Moved to snelpwi 4236 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 28924 
Virtual deduction proof of unipwr 28925. (Contributed by Alan Sare,
25Aug2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



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



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



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



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



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



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



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



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



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



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



18.25.7 Theorems proved using virtual deduction
with mmj2 assistance


Theorem  simplbi2VD 28938 
Virtual deduction proof of simplbi2 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:: 
 3:1,?: e0_ 28861 
 qed:3,?: e0_ 28861 

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



Theorem  3ornot23VD 28939 
Virtual deduction proof of 3ornot23 28569. 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_ 28704 
 4:1,?: e1_ 28704 
 5:3,4,?: e11 28765 
 6:2,?: e2 28708 
 7:5,6,?: e12 28813 
 8:7: 
 qed:8: 

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



Theorem  orbi1rVD 28940 
Virtual deduction proof of orbi1r 28570. 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 28708 
 4:1,3,?: e12 28813 
 5:4,?: e2 28708 
 6:5: 
 7:: 
 8:7,?: e2 28708 
 9:1,8,?: e12 28813 
 10:9,?: e2 28708 
 11:10: 
 12:6,11,?: e11 28765 
 qed:12: 

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



Theorem  bitr3VD 28941 
Virtual deduction proof of bitr3 28571. 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_ 28704 
 3:: 
 4:3,?: e2 28708 
 5:2,4,?: e12 28813 
 6:5: 
 qed:6: 

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



Theorem  3orbi123VD 28942 
Virtual deduction proof of 3orbi123 28572. 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_ 28704 
 3:1,?: e1_ 28704 
 4:1,?: e1_ 28704 
 5:2,3,?: e11 28765 
 6:5,4,?: e11 28765 
 7:?: 
 8:6,7,?: e10 28772 
 9:?: 
 10:8,9,?: e10 28772 
 qed:10: 

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



Theorem  sbc3orgVD 28943 
Virtual deduction proof of sbc3org 28594. 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_ 28704 
 3:: 
 32:3: 
 33:1,32,?: e10 28772 
 4:1,33,?: e11 28765 
 5:2,4,?: e11 28765 
 6:1,?: e1_ 28704 
 7:6,?: e1_ 28704 
 8:5,7,?: e11 28765 
 9:?: 
 10:8,9,?: e10 28772 
 qed:10: 

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



Theorem  19.21a3con13vVD 28944* 
Virtual deduction proof of alrim3con13v 28595. 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 28708 
 4:2,?: e2 28708 
 5:2,?: e2 28708 
 6:1,4,?: e12 28813 
 7:3,?: e2 28708 
 8:5,?: e2 28708 
 9:7,6,8,?: e222 28713 
 10:9,?: e2 28708 
 11:10:in2 
 qed:11:in1 

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



Theorem  exbirVD 28945 
Virtual deduction proof of exbir 1355. 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 28813 
 6:3,5,?: e32 28847 
 7:6: 
 8:7: 
 9:8,?: e1_ 28704 
 qed:9: 

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



Theorem  exbiriVD 28946 
Virtual deduction proof of exbiri 605. 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 28772 
 6:3,5,?: e21 28819 
 7:4,6,?: e32 28847 
 8:7: 
 9:8: 
 qed:9: 

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



Theorem  rspsbc2VD 28947* 
Virtual deduction proof of rspsbc2 28596. 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 28837 
 5:1,4,?: e13 28837 
 6:2,5,?: e23 28844 
 7:6: 
 8:7: 
 qed:8: 

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



Theorem  3impexpVD 28948 
Virtual deduction proof of 3impexp 1356. 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 28772 
 4:3,?: e1_ 28704 
 5:4,?: e1_ 28704 
 6:5: 
 7:: 
 8:7,?: e1_ 28704 
 9:8,?: e1_ 28704 
 10:2,9,?: e01 28768 
 11:10: 
 qed:6,11,?: e00 28857 

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



Theorem  3impexpbicomVD 28949 
Virtual deduction proof of 3impexpbicom 1357. 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 28772 
 4:3,?: e1_ 28704 
 5:4: 
 6:: 
 7:6,?: e1_ 28704 
 8:7,2,?: e10 28772 
 9:8: 
 qed:5,9,?: e00 28857 

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



Theorem  3impexpbicomiVD 28950 
Virtual deduction proof of 3impexpbicomi 1358. 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 28951* 
Virtual deduction proof of sbcoreleleq 28597. 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_ 28704 
 3:1,?: e1_ 28704 
 4:1,?: e1_ 28704 
 5:2,3,4,?: e111 28751 
 6:1,?: e1_ 28704 
 7:5,6: e11 28765 
 qed:7: 

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



Theorem  hbra2VD 28952* 
Virtual deduction proof of nfra2 2610. 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 28857 
 4:2: 
 5:4,?: e0_ 28861 
 qed:3,5,?: e00 28857 

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



Theorem  tratrbVD 28953* 
Virtual deduction proof of tratrb 28598. 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_ 28704 
 3:1,?: e1_ 28704 
 4:1,?: e1_ 28704 
 5:: 
 6:5,?: e2 28708 
 7:5,?: e2 28708 
 8:2,7,4,?: e121 28733 
 9:2,6,8,?: e122 28730 
 10:: 
 11:6,7,10,?: e223 28712 
 12:11: 
 13:: 
 14:12,13,?: e20 28816 
 15:: 
 16:7,15,?: e23 28844 
 17:6,16,?: e23 28844 
 18:17: 
 19:: 
 20:18,19,?: e20 28816 
 21:3,?: e1_ 28704 
 22:21,9,4,?: e121 28733 
 23:22,?: e2 28708 
 24:4,23,?: e12 28813 
 25:14,20,24,?: e222 28713 
 26:25: 
 27:: 
 28:27,?: e0_ 28861 
 29:28,26: 
 30:: 
 31:30,?: e0_ 28861 
 32:31,29: 
 33:32,?: e1_ 28704 
 qed:33: 

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



Theorem  3ax5VD 28954 
Virtual deduction proof of 3ax5 28599. 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_ 28704 
 3:: 
 4:2,3,?: e10 28772 
 qed:4: 

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



Theorem  syl5impVD 28955 
Virtual deduction proof of syl5imp 28573. 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_ 28704 
 3:: 
 4:3,2,?: e21 28819 
 5:4,?: e2 28708 
 6:5: 
 qed:6: 

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



Theorem  idiVD 28956 
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 28957 
Closed form of ancoms 439. 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 28958* 
Quantification restricted to a subclass for two quantifiers. ssralv 3250
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 28593 is ssralv2VD 28958 without
virtual deductions and was automatically derived from ssralv2VD 28958.
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 28959 
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36. This is an alternate proof of ordelord 4430 using
the Axiom of Regularity indirectly through dford2 7337. 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 28600 is ordelordALTVD 28959
without virtual deductions and was automatically derived from
ordelordALTVD 28959 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 28960 
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 3333 is equncomVD 28960 without
virtual deductions and was automatically derived from equncomVD 28960.
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 28961 
Inference form of equncom 3333. 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 3334 is equncomiVD 28961 without
virtual deductions and was automatically derived from equncomiVD 28961.
(Contributed by Alan Sare, 18Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sucidALTVD 28962 
A set belongs to its successor. Alternate proof of sucid 4487.
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 28963 is sucidALTVD 28962
without virtual deductions and was automatically derived from
sucidALTVD 28962. 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 4414, 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 7337.
h1:: 
 2:1: 
 3:2: 
 4:: 
 qed:3,4: 

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



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



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

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



Theorem  imbi12VD 28965 
Implication form of imbi12i 316. 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 28581
is imbi12VD 28965 without virtual deductions and was automatically derived
from imbi12VD 28965.
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 28966 
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 28582
is imbi13VD 28966 without virtual deductions and was automatically derived
from imbi13VD 28966.
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 28967 
Distribution of class substitution over a leftnested implication.
Similar
to sbcimg 3045. 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 28601
is sbcim2gVD 28967 without virtual deductions and was automatically derived
from sbcim2gVD 28967.
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 28968 
Implication form of sbcbiiOLD 3060. 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 28602
is sbcbiVD 28968 without virtual deductions and was automatically derived
from sbcbiVD 28968.
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 28969* 
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 28603
is trsbcVD 28969 without virtual deductions and was automatically derived
from trsbcVD 28969.
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 28970* 
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 28604
is truniALTVD 28970 without virtual deductions and was automatically derived
from truniALTVD 28970.
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 28971 
Nonvirtual deduction form of e33 28823. 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 28583
is ee33VD 28971 without virtual deductions and was automatically derived
from ee33VD 28971.
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 28972* 
The intersection of a class of transitive sets is transitive. Virtual
deduction proof of trintALT 28973.
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 28973
is trintALTVD 28972 without virtual deductions and was automatically derived
from trintALTVD 28972.
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 28973* 
The intersection of a class of transitive sets is transitive. Exercise
5(b) of [Enderton] p. 73. trintALT 28973 is an alternative proof of
trint 4144. trintALT 28973 is trintALTVD 28972 without virtual deductions and was
automatically derived from trintALTVD 28972 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 28974 
The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual
deduction proof of undif3 3442.
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 3442
is undif3VD 28974 without virtual deductions and was automatically derived
from undif3VD 28974.
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 28975 
Virtual deduction proof of sbcss 3577.
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 3577
is sbcssVD 28975 without virtual deductions and was automatically derived
from sbcssVD 28975.
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 28976 
Virtual deduction proof of csbing 3389.
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 3389
is csbingVD 28976 without virtual deductions and was automatically derived
from csbingVD 28976.
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 28977* 
Virtual deduction proof of onfrALTlem5 28606.
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 28606 is onfrALTlem5VD 28977 without virtual deductions and was
automatically derived
from onfrALTlem5VD 28977.
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: 
 16:15,14: 
 17:2: 
 18:2: 
 19:2: 
 20:18,19: 
 21:17,20: 
 22:2: 
 23:2: 
 24:21,23: 
 25:22,24: 
 26:2: 
 27:25,26: 
 28:2: 
 29:27,28: 
 30:29: 
 31:30: 
 32:: 
 