Type  Label  Description 
Statement 

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



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



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



16.22.4 Theorems proved using virtual
deduction


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



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



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



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



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



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



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



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



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



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



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



Theorem  snssl 27618 
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 3689.
The proof of
this theorem was automatically generated from snsslVD 27617 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 27619 
Virtual deduction proof of snelpwi 4158. (Contributed by Alan Sare,
25Aug2011.) (Proof modification is discouraged.)
(New usage is discouraged.)



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



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



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



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



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



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



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



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



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



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



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



16.22.5 Theorems proved using virtual deduction
with mmj2 assistance


Theorem  simplbi2VD 27635 
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_ 27560 
 qed:3,?: e0_ 27560 

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



Theorem  3ornot23VD 27636 
Virtual deduction proof of 3ornot23 27286. 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_ 27412 
 4:1,?: e1_ 27412 
 5:3,4,?: e11 27473 
 6:2,?: e2 27416 
 7:5,6,?: e12 27512 
 8:7: 
 qed:8: 

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



Theorem  orbi1rVD 27637 
Virtual deduction proof of orbi1r 27287. 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 27416 
 4:1,3,?: e12 27512 
 5:4,?: e2 27416 
 6:5: 
 7:: 
 8:7,?: e2 27416 
 9:1,8,?: e12 27512 
 10:9,?: e2 27416 
 11:10: 
 12:6,11,?: e11 27473 
 qed:12: 

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



Theorem  bitr3VD 27638 
Virtual deduction proof of bitr3 27288. 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_ 27412 
 3:: 
 4:3,?: e2 27416 
 5:2,4,?: e12 27512 
 6:5: 
 qed:6: 

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



Theorem  3orbi123VD 27639 
Virtual deduction proof of 3orbi123 27289. 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_ 27412 
 3:1,?: e1_ 27412 
 4:1,?: e1_ 27412 
 5:2,3,?: e11 27473 
 6:5,4,?: e11 27473 
 7:?: 
 8:6,7,?: e10 27480 
 9:?: 
 10:8,9,?: e10 27480 
 qed:10: 

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



Theorem  sbc3orgVD 27640 
Virtual deduction proof of sbc3org 27311. 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_ 27412 
 3:: 
 32:3: 
 33:1,32,?: e10 27480 
 4:1,33,?: e11 27473 
 5:2,4,?: e11 27473 
 6:1,?: e1_ 27412 
 7:6,?: e1_ 27412 
 8:5,7,?: e11 27473 
 9:?: 
 10:8,9,?: e10 27480 
 qed:10: 

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



Theorem  19.21a3con13vVD 27641* 
Virtual deduction proof of alrim3con13v 27312. 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 27416 
 4:2,?: e2 27416 
 5:2,?: e2 27416 
 6:1,4,?: e12 27512 
 7:3,?: e2 27416 
 8:5,?: e2 27416 
 9:7,6,8,?: e222 27421 
 10:9,?: e2 27416 
 11:10:in2 
 qed:11:in1 

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



Theorem  exbirVD 27642 
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 27512 
 6:3,5,?: e32 27546 
 7:6: 
 8:7: 
 9:8,?: e1_ 27412 
 qed:9: 

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



Theorem  exbiriVD 27643 
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 27480 
 6:3,5,?: e21 27518 
 7:4,6,?: e32 27546 
 8:7: 
 9:8: 
 qed:9: 

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



Theorem  ra4sbc2VD 27644* 
Virtual deduction proof of ra4sbc2 27313. 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 27536 
 5:1,4,?: e13 27536 
 6:2,5,?: e23 27543 
 7:6: 
 8:7: 
 qed:8: 

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



Theorem  3impexpVD 27645 
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 27480 
 4:3,?: e1_ 27412 
 5:4,?: e1_ 27412 
 6:5: 
 7:: 
 8:7,?: e1_ 27412 
 9:8,?: e1_ 27412 
 10:2,9,?: e01 27476 
 11:10: 
 qed:6,11,?: e00 27556 

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



Theorem  3impexpbicomVD 27646 
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 27480 
 4:3,?: e1_ 27412 
 5:4: 
 6:: 
 7:6,?: e1_ 27412 
 8:7,2,?: e10 27480 
 9:8: 
 qed:5,9,?: e00 27556 

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



Theorem  3impexpbicomiVD 27647 
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 27648* 
Virtual deduction proof of sbcoreleleq 27314. 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_ 27412 
 3:1,?: e1_ 27412 
 4:1,?: e1_ 27412 
 5:2,3,4,?: e111 27459 
 6:1,?: e1_ 27412 
 7:5,6: e11 27473 
 qed:7: 

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



Theorem  hbra2VD 27649* 
Virtual deduction proof of nfra2 2568. 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 27556 
 4:2: 
 5:4,?: e0_ 27560 
 qed:3,5,?: e00 27556 

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



Theorem  tratrbVD 27650* 
Virtual deduction proof of tratrb 27315. 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_ 27412 
 3:1,?: e1_ 27412 
 4:1,?: e1_ 27412 
 5:: 
 6:5,?: e2 27416 
 7:5,?: e2 27416 
 8:2,7,4,?: e121 27441 
 9:2,6,8,?: e122 27438 
 10:: 
 11:6,7,10,?: e223 27420 
 12:11: 
 13:: 
 14:12,13,?: e20 27515 
 15:: 
 16:7,15,?: e23 27543 
 17:6,16,?: e23 27543 
 18:17: 
 19:: 
 20:18,19,?: e20 27515 
 21:3,?: e1_ 27412 
 22:21,9,4,?: e121 27441 
 23:22,?: e2 27416 
 24:4,23,?: e12 27512 
 25:14,20,24,?: e222 27421 
 26:25: 
 27:: 
 28:27,?: e0_ 27560 
 29:28,26: 
 30:: 
 31:30,?: e0_ 27560 
 32:31,29: 
 33:32,?: e1_ 27412 
 qed:33: 

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



Theorem  3ax5VD 27651 
Virtual deduction proof of 3ax5 27316. 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_ 27412 
 3:: 
 4:2,3,?: e10 27480 
 qed:4: 

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



Theorem  syl5impVD 27652 
Virtual deduction proof of syl5imp 27290. 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_ 27412 
 3:: 
 4:3,2,?: e21 27518 
 5:4,?: e2 27416 
 6:5: 
 qed:6: 

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



Theorem  idiVD 27653 
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 27654 
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 27655* 
Quantification restricted to a subclass for two quantifiers. ssralv 3179
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 27310 is ssralv2VD 27655 without
virtual deductions and was automatically derived from ssralv2VD 27655.
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 27656 
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36. This is an alternate proof of ordelord 4351 using
the Axiom of Regularity indirectly through dford2 7254. 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 27317 is ordelordALTVD 27656
without virtual deductions and was automatically derived from
ordelordALTVD 27656 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 27657 
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 3262 is equncomVD 27657 without
virtual deductions and was automatically derived from equncomVD 27657.
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 27658 
Inference form of equncom 3262. 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 3263 is equncomiVD 27658 without
virtual deductions and was automatically derived from equncomiVD 27658.
(Contributed by Alan Sare, 18Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sucidALTVD 27659 
A set belongs to its successor. Alternate proof of sucid 4408.
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 27660 is sucidALTVD 27659
without virtual deductions and was automatically derived from
sucidALTVD 27659. 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 4335, 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 7254.
h1:: 
 2:1: 
 3:2: 
 4:: 
 qed:3,4: 

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



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



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

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



Theorem  imbi12VD 27662 
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 27298
is imbi12VD 27662 without virtual deductions and was automatically derived
from imbi12VD 27662.
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 27663 
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 27299
is imbi13VD 27663 without virtual deductions and was automatically derived
from imbi13VD 27663.
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 27664 
Distribution of class substitution over a leftnested implication.
Similar
to sbcimg 2976. 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 27318
is sbcim2gVD 27664 without virtual deductions and was automatically derived
from sbcim2gVD 27664.
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 27665 
Implication form of sbcbiiOLD 2991. 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 27319
is sbcbiVD 27665 without virtual deductions and was automatically derived
from sbcbiVD 27665.
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 27666* 
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 27320
is trsbcVD 27666 without virtual deductions and was automatically derived
from trsbcVD 27666.
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 27667* 
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 27321
is truniALTVD 27667 without virtual deductions and was automatically derived
from truniALTVD 27667.
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 27668 
Nonvirtual deduction form of e33 27522. 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 27300
is ee33VD 27668 without virtual deductions and was automatically derived
from ee33VD 27668.
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 27669* 
The intersection of a class of transitive sets is transitive. Virtual
deduction proof of trintALT 27670.
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 27670
is trintALTVD 27669 without virtual deductions and was automatically derived
from trintALTVD 27669.
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 27670* 
The intersection of a class of transitive sets is transitive. Exercise
5(b) of [Enderton] p. 73. trintALT 27670 is an alternative proof of
trint 4068. trintALT 27670 is trintALTVD 27669 without virtual deductions and was
automatically derived from trintALTVD 27669 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 27671 
The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual
deduction proof of undif3 3371.
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 3371
is undif3VD 27671 without virtual deductions and was automatically derived
from undif3VD 27671.
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 27672 
Virtual deduction proof of sbcss 27322.
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 27322
is sbcssVD 27672 without virtual deductions and was automatically derived
from sbcssVD 27672.
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 27673 
Virtual deduction proof of csbing 3318.
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 3318
is csbingVD 27673 without virtual deductions and was automatically derived
from csbingVD 27673.
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 27674* 
Virtual deduction proof of onfrALTlem5 27323.
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 27323 is onfrALTlem5VD 27674 without virtual deductions and was
automatically derived
from onfrALTlem5VD 27674.
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::   