Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



16.21.5 Theorems proved using virtual deduction
with mmj2 assistance


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

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



Theorem  3ornot23VD 27410 
Virtual deduction proof of 3ornot23 27060. 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_ 27186 
 4:1,?: e1_ 27186 
 5:3,4,?: e11 27247 
 6:2,?: e2 27190 
 7:5,6,?: e12 27286 
 8:7: 
 qed:8: 

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



Theorem  orbi1rVD 27411 
Virtual deduction proof of orbi1r 27061. 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 27190 
 4:1,3,?: e12 27286 
 5:4,?: e2 27190 
 6:5: 
 7:: 
 8:7,?: e2 27190 
 9:1,8,?: e12 27286 
 10:9,?: e2 27190 
 11:10: 
 12:6,11,?: e11 27247 
 qed:12: 

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



Theorem  bitr3VD 27412 
Virtual deduction proof of bitr3 27062. 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_ 27186 
 3:: 
 4:3,?: e2 27190 
 5:2,4,?: e12 27286 
 6:5: 
 qed:6: 

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



Theorem  3orbi123VD 27413 
Virtual deduction proof of 3orbi123 27063. 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_ 27186 
 3:1,?: e1_ 27186 
 4:1,?: e1_ 27186 
 5:2,3,?: e11 27247 
 6:5,4,?: e11 27247 
 7:?: 
 8:6,7,?: e10 27254 
 9:?: 
 10:8,9,?: e10 27254 
 qed:10: 

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



Theorem  sbc3orgVD 27414 
Virtual deduction proof of sbc3org 27085. 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_ 27186 
 3:: 
 32:3: 
 33:1,32,?: e10 27254 
 4:1,33,?: e11 27247 
 5:2,4,?: e11 27247 
 6:1,?: e1_ 27186 
 7:6,?: e1_ 27186 
 8:5,7,?: e11 27247 
 9:?: 
 10:8,9,?: e10 27254 
 qed:10: 

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



Theorem  19.21a3con13vVD 27415* 
Virtual deduction proof of alrim3con13v 27086. 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 27190 
 4:2,?: e2 27190 
 5:2,?: e2 27190 
 6:1,4,?: e12 27286 
 7:3,?: e2 27190 
 8:5,?: e2 27190 
 9:7,6,8,?: e222 27195 
 10:9,?: e2 27190 
 11:10:in2 
 qed:11:in1 

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



Theorem  exbirVD 27416 
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 27286 
 6:3,5,?: e32 27320 
 7:6: 
 8:7: 
 9:8,?: e1_ 27186 
 qed:9: 

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



Theorem  exbiriVD 27417 
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 27254 
 6:3,5,?: e21 27292 
 7:4,6,?: e32 27320 
 8:7: 
 9:8: 
 qed:9: 

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



Theorem  ra4sbc2VD 27418* 
Virtual deduction proof of ra4sbc2 27087. 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 27310 
 5:1,4,?: e13 27310 
 6:2,5,?: e23 27317 
 7:6: 
 8:7: 
 qed:8: 

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



Theorem  3impexpVD 27419 
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 27254 
 4:3,?: e1_ 27186 
 5:4,?: e1_ 27186 
 6:5: 
 7:: 
 8:7,?: e1_ 27186 
 9:8,?: e1_ 27186 
 10:2,9,?: e01 27250 
 11:10: 
 qed:6,11,?: e00 27330 

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



Theorem  3impexpbicomVD 27420 
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 27254 
 4:3,?: e1_ 27186 
 5:4: 
 6:: 
 7:6,?: e1_ 27186 
 8:7,2,?: e10 27254 
 9:8: 
 qed:5,9,?: e00 27330 

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



Theorem  3impexpbicomiVD 27421 
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 27422* 
Virtual deduction proof of sbcoreleleq 27088. 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_ 27186 
 3:1,?: e1_ 27186 
 4:1,?: e1_ 27186 
 5:2,3,4,?: e111 27233 
 6:1,?: e1_ 27186 
 7:5,6: e11 27247 
 qed:7: 

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



Theorem  hbra2VD 27423* 
Virtual deduction proof of nfra2 2559. 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 27330 
 4:2: 
 5:4,?: e0_ 27334 
 qed:3,5,?: e00 27330 

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



Theorem  tratrbVD 27424* 
Virtual deduction proof of tratrb 27089. 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_ 27186 
 3:1,?: e1_ 27186 
 4:1,?: e1_ 27186 
 5:: 
 6:5,?: e2 27190 
 7:5,?: e2 27190 
 8:2,7,4,?: e121 27215 
 9:2,6,8,?: e122 27212 
 10:: 
 11:6,7,10,?: e223 27194 
 12:11: 
 13:: 
 14:12,13,?: e20 27289 
 15:: 
 16:7,15,?: e23 27317 
 17:6,16,?: e23 27317 
 18:17: 
 19:: 
 20:18,19,?: e20 27289 
 21:3,?: e1_ 27186 
 22:21,9,4,?: e121 27215 
 23:22,?: e2 27190 
 24:4,23,?: e12 27286 
 25:14,20,24,?: e222 27195 
 26:25: 
 27:: 
 28:27,?: e0_ 27334 
 29:28,26: 
 30:: 
 31:30,?: e0_ 27334 
 32:31,29: 
 33:32,?: e1_ 27186 
 qed:33: 

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



Theorem  3ax5VD 27425 
Virtual deduction proof of 3ax5 27090. 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_ 27186 
 3:: 
 4:2,3,?: e10 27254 
 qed:4: 

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



Theorem  syl5impVD 27426 
Virtual deduction proof of syl5imp 27064. 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_ 27186 
 3:: 
 4:3,2,?: e21 27292 
 5:4,?: e2 27190 
 6:5: 
 qed:6: 

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



Theorem  idiVD 27427 
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 27428 
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 27429* 
Quantification restricted to a subclass for two quantifiers. ssralv 3158
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 27084 is ssralv2VD 27429 without
virtual deductions and was automatically derived from ssralv2VD 27429.
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 27430 
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36. This is an alternate proof of ordelord 4307 using
the Axiom of Regularity indirectly through dford2 7205. 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 27091 is ordelordALTVD 27430
without virtual deductions and was automatically derived from
ordelordALTVD 27430 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 27431 
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 3230 is equncomVD 27431 without
virtual deductions and was automatically derived from equncomVD 27431.
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 27432 
Inference form of equncom 3230. 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 3231 is equncomiVD 27432 without
virtual deductions and was automatically derived from equncomiVD 27432.
(Contributed by Alan Sare, 18Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sucidALTVD 27433 
A set belongs to its successor. Alternate proof of sucid 4364.
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 27434 is sucidALTVD 27433
without virtual deductions and was automatically derived from
sucidALTVD 27433. 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 4291, 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 7205.
h1:: 
 2:1: 
 3:2: 
 4:: 
 qed:3,4: 

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



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



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

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



Theorem  imbi12VD 27436 
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 27072
is imbi12VD 27436 without virtual deductions and was automatically derived
from imbi12VD 27436.
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 27437 
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 27073
is imbi13VD 27437 without virtual deductions and was automatically derived
from imbi13VD 27437.
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 27438 
Distribution of class substitution over a leftnested implication.
Similar
to sbcimg 2962. 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 27092
is sbcim2gVD 27438 without virtual deductions and was automatically derived
from sbcim2gVD 27438.
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 27439 
Implication form of sbcbiiOLD 2977. 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 27093
is sbcbiVD 27439 without virtual deductions and was automatically derived
from sbcbiVD 27439.
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 27440* 
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 27094
is trsbcVD 27440 without virtual deductions and was automatically derived
from trsbcVD 27440.
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 27441* 
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 27095
is truniALTVD 27441 without virtual deductions and was automatically derived
from truniALTVD 27441.
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 27442 
Nonvirtual deduction form of e33 27296. 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 27074
is ee33VD 27442 without virtual deductions and was automatically derived
from ee33VD 27442.
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 27443* 
The intersection of a class of transitive sets is transitive. Virtual
deduction proof of trintALT 27444.
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 27444
is trintALTVD 27443 without virtual deductions and was automatically derived
from trintALTVD 27443.
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 27444* 
The intersection of a class of transitive sets is transitive. Exercise
5(b) of [Enderton] p. 73. trintALT 27444 is an alternative proof of
trint 4025. trintALT 27444 is trintALTVD 27443 without virtual deductions and was
automatically derived from trintALTVD 27443 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 27445 
The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual
deduction proof of undif3 3336.
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 3336
is undif3VD 27445 without virtual deductions and was automatically derived
from undif3VD 27445.
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 27446 
Virtual deduction proof of sbcss 27096.
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 27096
is sbcssVD 27446 without virtual deductions and was automatically derived
from sbcssVD 27446.
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 27447 
Virtual deduction proof of csbing 3283.
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 3283
is csbingVD 27447 without virtual deductions and was automatically derived
from csbingVD 27447.
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 27448* 
Virtual deduction proof of onfrALTlem5 27097.
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 27097 is onfrALTlem5VD 27448 without virtual deductions and was
automatically derived
from onfrALTlem5VD 27448.
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:: 
 33:31,32: 
 34:2: 
 35:33,34: 
 36:: 
 37:36: 
 38:2,37: 
 39:35,38: 
 40:16,39: 
 41:2: 
 qed:40,41: 

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



Theorem  onfrALTlem4VD 27449* 
Virtual deduction proof of onfrALTlem4 27098.
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. onfrALTlem4 27098
is onfrALTlem4VD 27449 without virtual deductions and was automatically
derived
from onfrALTlem4VD 27449.
1:: 
 2:1: 
 3:1: 
 4:1: 
 5:1: 
 6:4,5: 
 7:3,6: 
 8:1: 
 9:7,8:   