Type  Label  Description 
Statement 

Theorem  trintALTVD 28701* 
The intersection of a class of transitive sets is transitive. Virtual
deduction proof of trintALT 28702.
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 28702
is trintALTVD 28701 without virtual deductions and was automatically derived
from trintALTVD 28701.
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 28702* 
The intersection of a class of transitive sets is transitive. Exercise
5(b) of [Enderton] p. 73. trintALT 28702 is an alternative proof of
trint 4277. trintALT 28702 is trintALTVD 28701 without virtual deductions and was
automatically derived from trintALTVD 28701 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 28703 
The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual
deduction proof of undif3 3562.
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 3562
is undif3VD 28703 without virtual deductions and was automatically derived
from undif3VD 28703.
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 28704 
Virtual deduction proof of sbcss 3698.
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 3698
is sbcssVD 28704 without virtual deductions and was automatically derived
from sbcssVD 28704.
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 28705 
Virtual deduction proof of csbing 3508.
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 3508
is csbingVD 28705 without virtual deductions and was automatically derived
from csbingVD 28705.
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 28706* 
Virtual deduction proof of onfrALTlem5 28339.
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 28339 is onfrALTlem5VD 28706 without virtual deductions and was
automatically derived
from onfrALTlem5VD 28706.
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 28707* 
Virtual deduction proof of onfrALTlem4 28340.
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 28340
is onfrALTlem4VD 28707 without virtual deductions and was automatically
derived
from onfrALTlem4VD 28707.
1:: 
 2:1: 
 3:1: 
 4:1: 
 5:1: 
 6:4,5: 
 7:3,6: 
 8:1: 
 9:7,8: 
 10:2,9: 
 11:1: 
 12:11,10: 
 13:1: 
 qed:13,12: 

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



Theorem  onfrALTlem3VD 28708* 
Virtual deduction proof of onfrALTlem3 28341.
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. onfrALTlem3 28341
is onfrALTlem3VD 28708 without virtual deductions and was automatically
derived
from onfrALTlem3VD 28708.
1:: 
 2:: 
 3:2: 
 4:1: 
 5:3,4: 
 6:5: 
 7:6: 
 8:: 
 9:7,8: 
 10:9: 
 11:10: 
 12:: 
 13:12,8: 
 14:13,11: 
 15:: 
 16:14,15: 
 17:: 
 18:2: 
 19:18: 
 20:17,19: 
 qed:16,20: 

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



Theorem  simplbi2comgVD 28709 
Virtual deduction proof of simplbi2comg 1379.
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. simplbi2comg 1379
is simplbi2comgVD 28709 without virtual deductions and was automatically
derived
from simplbi2comgVD 28709.
1:: 
 2:1: 
 3:2: 
 4:3: 
 qed:4: 

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



Theorem  onfrALTlem2VD 28710* 
Virtual deduction proof of onfrALTlem2 28343.
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. onfrALTlem2 28343
is onfrALTlem2VD 28710 without virtual deductions and was automatically
derived
from onfrALTlem2VD 28710.
1:: 
 2:1: 
 3:2: 
 4:: 
 5:: 
 6:5: 
 7:4: 
 8:6,7: 
 9:8: 
 10:9: 
 11:1: 
 12:11: 
 13:2: 
 14:10,12,13: 
 15:3,14: 
 16:13,15: 
 17:16: 
 18:17: 
 19:18: 
 20:: 
 21:20: 
 22:19,21: 
 23:20: 
 24:23: 
 25:22,24: 
 26:25: 
 27:26: 
 28:27: 
 29:: 
 30:29: 
 31:28,30: 
 qed:31: 

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



Theorem  onfrALTlem1VD 28711* 
Virtual deduction proof of onfrALTlem1 28345.
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. onfrALTlem1 28345
is onfrALTlem1VD 28711 without virtual deductions and was automatically
derived
from onfrALTlem1VD 28711.
1:: 
 2:1: 
 3:2: 
 4:: 
 5:4: 
 6:5: 
 7:3,6: 
 8:: 
 qed:7,8: 

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



Theorem  onfrALTVD 28712 
Virtual deduction proof of onfrALT 28346.
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. onfrALT 28346
is onfrALTVD 28712 without virtual deductions and was automatically derived
from onfrALTVD 28712.
1:: 
 2:: 
 3:1: 
 4:2: 
 5:: 
 6:5,4,3: 
 7:6: 
 8:7: 
 9:8: 
 10:: 
 11:9,10: 
 12:: 
 13:12: 
 14:13,11: 
 15:14: 
 16:15: 
 qed:16: 

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



Theorem  csbeq2gVD 28713 
Virtual deduction proof of csbeq2g 28347.
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. csbeq2g 28347
is csbeq2gVD 28713 without virtual deductions and was automatically derived
from csbeq2gVD 28713.
1:: 
 2:1: 
 3:1: 
 4:2,3: 
 qed:4: 

(Contributed by Alan Sare, 10Nov2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



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

(Contributed by Alan Sare, 10Nov2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  csbxpgVD 28715 
Virtual deduction proof of csbxpg 4864.
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. csbxpg 4864
is csbxpgVD 28715 without virtual deductions and was automatically derived
from csbxpgVD 28715.
1:: 
 2:1: 
 3:1: 
 4:3: 
 5:2,4: 
 6:1: 
 7:1: 
 8:7: 
 9:6,8: 
 10:5,9: 
 11:1: 
 12:10,11: 
 13:1: 
 14:12,13: 
 15:1: 
 16:14,15: 
 17:16: 
 18:17: 
 19:1: 
 20:18,19: 
 21:20: 
 22:21: 
 23:1: 
 24:22,23: 
 25:24: 
 26:25: 
 27:1: 
 28:26,27: 
 29:: 
 30:: 
 31:29,30: 
 32:31: 
 33:1,32: 
 34:28,33: 
 35:: 
 36:: 
 37:35,36: 
 38:34,37: 
 qed:38: 

(Contributed by Alan Sare, 10Nov2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  csbresgVD 28716 
Virtual deduction proof of csbresg 5108.
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. csbresg 5108
is csbresgVD 28716 without virtual deductions and was automatically derived
from csbresgVD 28716.
1:: 
 2:1: 
 3:2: 
 4:1: 
 5:3,4: 
 6:5: 
 7:1: 
 8:6,7: 
 9:: 
 10:9: 
 11:1,10: 
 12:8,11: 
 13:: 
 14:12,13: 
 qed:14: 

(Contributed by Alan Sare, 10Nov2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  csbrngVD 28717 
Virtual deduction proof of csbrng 5073.
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. csbrng 5073
is csbrngVD 28717 without virtual deductions and was automatically derived
from csbrngVD 28717.
1:: 
 2:1: 
 3:1: 
 4:3: 
 5:2,4: 
 6:5: 
 7:6: 
 8:1: 
 9:7,8: 
 10:9: 
 11:10: 
 12:1: 
 13:11,12: 
 14:: 
 15:14: 
 16:1,15: 
 17:13,16: 
 18:: 
 19:17,18: 
 qed:19: 

(Contributed by Alan Sare, 10Nov2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  csbima12gALTVD 28718 
Virtual deduction proof of csbima12gALT 5173.
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. csbima12gALT 5173
is csbima12gALTVD 28718 without virtual deductions and was automatically
derived
from csbima12gALTVD 28718.
1:: 
 2:1: 
 3:2: 
 4:1: 
 5:3,4: 
 6:: 
 7:6: 
 8:1,7: 
 9:5,8: 
 10:: 
 11:9,10: 
 qed:11: 

(Contributed by Alan Sare, 10Nov2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  csbunigVD 28719 
Virtual deduction proof of csbunig 3983.
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. csbunig 3983
is csbunigVD 28719 without virtual deductions and was automatically derived
from csbunigVD 28719.
1:: 
 2:1: 
 3:1: 
 4:2,3: 
 5:1: 
 6:4,5: 
 7:6: 
 8:7: 
 9:1: 
 10:8,9: 
 11:10: 
 12:11: 
 13:1: 
 14:12,13: 
 15:: 
 16:15: 
 17:1,16: 
 18:1,17: 
 19:14,18: 
 20:: 
 21:19,20: 
 qed:21: 

(Contributed by Alan Sare, 10Nov2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  csbfv12gALTVD 28720 
Virtual deduction proof of csbfv12gALT 5698.
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. csbfv12gALT 5698
is csbfv12gALTVD 28720 without virtual deductions and was automatically
derived
from csbfv12gALTVD 28720.
1:: 
 2:1: 
 3:1: 
 4:1: 
 5:4: 
 6:3,5: 
 7:1: 
 8:6,2: 
 9:7,8: 
 10:9: 
 11:10: 
 12:1: 
 13:11,12: 
 14:13: 
 15:1: 
 16:14,15: 
 17:: 
 18:17: 
 19:1,18: 
 20:16,19: 
 21:: 
 22:20,21: 
 qed:22: 

(Contributed by Alan Sare, 10Nov2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  con5VD 28721 
Virtual deduction proof of con5 28317.
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. con5 28317
is con5VD 28721 without virtual deductions and was automatically derived
from con5VD 28721.
1:: 
 2:1: 
 3:2: 
 4:: 
 5:3,4: 
 qed:5: 

(Contributed by Alan Sare, 21Apr2013.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  relopabVD 28722 
Virtual deduction proof of relopab 4960.
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. relopab 4960
is relopabVD 28722 without virtual deductions and was automatically derived
from relopabVD 28722.
1:: 
 2:1: 
 3:: 
 4:3: 
 5:2,4: 
 6:5: 
 7:6: 
 8:7: 
 9:8: 
 90:: 
 91:90: 
 92:: 
 10:91,92: 
 11:9,10: 
 12:11: 
 13:: 
 14:12,13: 
 15:14: 
 150:: 
 151:150: 
 152:: 
 16:151,152: 
 17:15,16: 
 18:17: 
 19:18: 
 20:: 
 21:19,20: 
 22:21: 
 23:: 
 24:22,23: 
 25:24: 
 26:: 
 27:: 
 28:26,27: 
 29:28: 
 30:29: 
 31:30: 
 32:31: 
 320:25,32: 
 33:: 
 34:: 
 35:33,34: 
 36:35: 
 37:36: 
 38:37: 
 39:38: 
 40:320,39: 
 41:: 
 42:: 
 43:40,41,42: 
 44:: 
 45:43,44: 
 46:28: 
 47:46: 
 48:45,47: 
 qed:48: 

(Contributed by Alan Sare, 9Jul2013.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  19.41rgVD 28723 
Virtual deduction proof of 19.41rg 28348.
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. 19.41rg 28348
is 19.41rgVD 28723 without virtual deductions and was automatically derived
from 19.41rgVD 28723. (Contributed by Alan Sare, 8Feb2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
1:: 
 2:1: 
 3:2: 
 4:3: 
 5:: 
 6:4,5: 
 7:: 
 8:6,7: 
 9:8: 
 10:9: 
 11:5: 
 12:10,11: 
 13:12: 
 14:13: 
 qed:14: 




Theorem  2pm13.193VD 28724 
Virtual deduction proof of 2pm13.193 28350.
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. 2pm13.193 28350
is 2pm13.193VD 28724 without virtual deductions and was automatically
derived from 2pm13.193VD 28724. (Contributed by Alan Sare, 8Feb2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
1:: 
 2:1: 
 3:2: 
 4:1: 
 5:3,4: 
 6:5: 
 7:6: 
 8:2:   