Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  csbfv12gALTVD Unicode version

Theorem csbfv12gALTVD 30481
Description: Virtual deduction proof of csbfv12gALTOLD 30404. 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. csbfv12gALTOLD 30404 is csbfv12gALTVD 30481 without virtual deductions and was automatically derived from csbfv12gALTVD 30481.
 1:: |-(.Ae. ->.Ae. ). 2:1: |-(.Ae. ->.[_A ]_{ }={ }). 3:1: |-(.Ae. ->.[_A ]_( "{B })=([_A ]_ "[_A ]_{B})). 4:1: |-(.Ae. ->.[_A ]_{B}={ [_A ]_B}). 5:4: |-(.Ae. ->.([_A ]_ "[_A ]_{B})=([_A ]_ "{[_A ]_B})). 6:3,5: |-(.Ae. ->.[_A ]_( "{B })=([_A ]_ "{[_A ]_B})). 7:1: |-(.Ae. ->.([.A ].( "{ B})={ }<->[_A ]_( "{B})=[_A ]_{ })). 8:6,2: |-(.Ae. ->.([_A ]_( "{ B})=[_A ]_{ }<->([_A ]_ "{[_A ]_B}) ={ })). 9:7,8: |-(.Ae. ->.([.A ].( "{ B})={ }<->([_A ]_ "{[_A ]_B})={ }) ). 10:9: |-(.Ae. ->.A. ([.A ].( "{B})={ }<->([_A ]_ "{[_A ]_B})= { })). 11:10: |-(.Ae. ->.{ |[.A ].( "{B})={ }}={ |([_A ]_ "{[_A ]_B})= { }}). 12:1: |-(.Ae. ->.[_A ]_{ |( "{B})={ }}={ |[.A ].( "{B})={ }}). 13:11,12: |-(.Ae. ->.[_A ]_{ |( "{B})={ }}={ |([_A ]_ "{[_A ]_B})= { }}). 14:13: |-(.Ae. ->.U.[_A ]_{ |( "{B})={ }}=U.{ |([_A ]_ " {[_A ]_B})= { }}). 15:1: |-(.Ae. ->.[_A ]_U.{ |( "{B})={ }}=U.[_A ]_{ |( "{B})= { }}). 16:14,15: |-(.Ae. ->.[_A ]_U.{ |( "{B})={ }}= U.{ |([_A ]_ "{[_A ]_B})= { }}). 17:: |-( B)= U.{ |( "{B})= { }} 18:17: |-A. ( B)=U.{ |( "{B })={ }} 19:1,18: |-(.Ae. ->.[_A ]_( B) =[_A ]_U.{ |( "{B})={ }}). 20:16,19: |-(.Ae. ->.[_A ]_( B) =U.{ |([_A ]_ "{[_A ]_B})={ }}). 21:: |-([_A ]_ [_A ]_B)= 22:20,21: |-(.Ae. ->.[_A ]_( B) =([_A ]_ [_A ]_B)). qed:22: |-(Ae. ->[_A ]_( B)= ([_A ]_ [_A ]_B))
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbfv12gALTVD

Proof of Theorem csbfv12gALTVD
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 idn1 30133 . . . . . . . . . . 11
2 sbceqg 3712 . . . . . . . . . . 11
31, 2e1_ 30196 . . . . . . . . . 10
4 csbima12gOLD 5210 . . . . . . . . . . . . 13
51, 4e1_ 30196 . . . . . . . . . . . 12
6 csbsng 3967 . . . . . . . . . . . . . 14
71, 6e1_ 30196 . . . . . . . . . . . . 13
8 imaeq2 5188 . . . . . . . . . . . . 13
97, 8e1_ 30196 . . . . . . . . . . . 12
10 eqeq1 2495 . . . . . . . . . . . . 13
1110biimprd 216 . . . . . . . . . . . 12
125, 9, 11e11 30257 . . . . . . . . . . 11
13 csbconstg 3338 . . . . . . . . . . . 12
141, 13e1_ 30196 . . . . . . . . . . 11
15 eqeq12 2501 . . . . . . . . . . . 12
1615ex 425 . . . . . . . . . . 11
1712, 14, 16e11 30257 . . . . . . . . . 10
18 bibi1 319 . . . . . . . . . . 11
1918biimprd 216 . . . . . . . . . 10
203, 17, 19e11 30257 . . . . . . . . 9
2120gen11 30185 . . . . . . . 8
22 abbi 2599 . . . . . . . . 9
2322biimpi 188 . . . . . . . 8
2421, 23e1_ 30196 . . . . . . 7
25 csbabgOLD 3743 . . . . . . . 8
261, 25e1_ 30196 . . . . . . 7
27 eqeq2 2498 . . . . . . . 8
2827biimpd 200 . . . . . . 7
2924, 26, 28e11 30257 . . . . . 6
30 unieq 4125 . . . . . 6
3129, 30e1_ 30196 . . . . 5
32 csbunigOLD 4146 . . . . . 6
331, 32e1_ 30196 . . . . 5
34 eqeq2 2498 . . . . . 6
3534biimpd 200 . . . . 5
3631, 33, 35e11 30257 . . . 4
37 dffv4 5705 . . . . . 6
3837ax-gen 1570 . . . . 5
39 csbeq2gOLD 30104 . . . . 5
401, 38, 39e10 30263 . . . 4
41 eqeq2 2498 . . . . 5
4241biimpd 200 . . . 4
4336, 40, 42e11 30257 . . 3
44 dffv4 5705 . . 3
45 eqeq2 2498 . . . 4
4645biimprcd 218 . . 3
4743, 44, 46e10 30263 . 2
4847in1 30130 1
 Colors of variables: wff set class Syntax hints:  ->wi 4  <->wb 178  A.wal 1564  =wceq 1670  e.wcel 1732  {cab 2475  [.wsbc 3224  [_csb 3325  {csn 3909  U.cuni 4117  "cima 4865  cfv 5438 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1338  df-fal 1339  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-ral 2764  df-rex 2765  df-rab 2768  df-v 3017  df-sbc 3225  df-csb 3326  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-if 3826  df-sn 3915  df-pr 3916  df-op 3918  df-uni 4118  df-br 4319  df-opab 4377  df-xp 4868  df-cnv 4870  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-iota 5401  df-fv 5446  df-vd1 30129
 Copyright terms: Public domain W3C validator