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

Theorem csbfv12gALTVD 29408
Description: Virtual deduction proof of csbfv12gALTOLD 29331. 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 29331 is csbfv12gALTVD 29408 without virtual deductions and was automatically derived from csbfv12gALTVD 29408.
1:: |-(. e. ->. e. ).
2:1: |-(. e. ->.[_ ]_{ }={ }).
3:1: |-(. e. ->.[_ ]_( "{ })=([_ ]_ "[_ ]_{ })).
4:1: |-(. e. ->.[_ ]_{ }={ [_ ]_ }).
5:4: |-(. e. ->.([_ ]_ "[_ ]_{ })=([_ ]_ "{[_ ]_ })).
6:3,5: |-(. e. ->.[_ ]_( "{ })=([_ ]_ "{[_ ]_ })).
7:1: |-(. e. ->.([. ].( "{ })={ }<->[_ ]_( "{ })=[_ ]_{ })).
8:6,2: |-(. e. ->.([_ ]_( "{ })=[_ ]_{ }<->([_ ]_ "{[_ ]_ }) ={ })).
9:7,8: |-(. e. ->.([. ].( "{ })={ }<->([_ ]_ "{[_ ]_ })={ }) ).
10:9: |-(. e. ->.A. ([. ].( "{ })={ }<->([_ ]_ "{[_ ]_ })= { })).
11:10: |-(. e. ->.{ |[. ].( "{ })={ }}={ |([_ ]_ "{[_ ]_ })= { }}).
12:1: |-(. e. ->.[_ ]_{ |( "{ })={ }}={ |[. ].( "{ })={ }}).
13:11,12: |-(. e. ->.[_ ]_{ |( "{ })={ }}={ |([_ ]_ "{[_ ]_ })= { }}).
14:13: |-(. e. ->.U.[_ ]_{ |( "{ })={ }}=U.{ |([_ ]_ " {[_ ]_ })= { }}).
15:1: |-(. e. ->.[_ ]_U.{ |( "{ })={ }}=U.[_ ]_{ |( "{ })= { }}).
16:14,15: |-(. e. ->.[_ ]_U.{ |( "{ })={ }}= U.{ |([_ ]_ "{[_ ]_ })= { }}).
17:: |-( ` )= U.{ |( "{ })= { }}
18:17: |-A. ( ` )=U.{ |( "{ })={ }}
19:1,18: |-(. e. ->.[_ ]_( ` ) =[_ ]_U.{ |( "{ })={ }}).
20:16,19: |-(. e. ->.[_ ]_( ` ) =U.{ |([_ ]_ "{[_ ]_ })={ }}).
21:: |-([_ ]_ `[_ ]_ )=
22:20,21: |-(. e. ->.[_ ]_( ` ) =([_ ]_ `[_ ]_ )).
qed:22: |-( e. ->[_ ]_( ` )= ([_ ]_ `[_ ]_ ))
(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 29060 . . . . . . . . . . 11
2 sbceqg 3659 . . . . . . . . . . 11
31, 2e1_ 29123 . . . . . . . . . 10
4 csbima12gOLD 5270 . . . . . . . . . . . . 13
51, 4e1_ 29123 . . . . . . . . . . . 12
6 csbsng 3899 . . . . . . . . . . . . . 14
71, 6e1_ 29123 . . . . . . . . . . . . 13
8 imaeq2 5247 . . . . . . . . . . . . 13
97, 8e1_ 29123 . . . . . . . . . . . 12
10 eqeq1 2453 . . . . . . . . . . . . 13
1110biimprd 216 . . . . . . . . . . . 12
125, 9, 11e11 29184 . . . . . . . . . . 11
13 csbconstg 3286 . . . . . . . . . . . 12
141, 13e1_ 29123 . . . . . . . . . . 11
15 eqeq12 2459 . . . . . . . . . . . 12
1615ex 425 . . . . . . . . . . 11
1712, 14, 16e11 29184 . . . . . . . . . 10
18 bibi1 319 . . . . . . . . . . 11
1918biimprd 216 . . . . . . . . . 10
203, 17, 19e11 29184 . . . . . . . . 9
2120gen11 29112 . . . . . . . 8
22 abbi 2557 . . . . . . . . 9
2322biimpi 188 . . . . . . . 8
2421, 23e1_ 29123 . . . . . . 7
25 csbabgOLD 3690 . . . . . . . 8
261, 25e1_ 29123 . . . . . . 7
27 eqeq2 2456 . . . . . . . 8
2827biimpd 200 . . . . . . 7
2924, 26, 28e11 29184 . . . . . 6
30 unieq 4055 . . . . . 6
3129, 30e1_ 29123 . . . . 5
32 csbunigOLD 4075 . . . . . 6
331, 32e1_ 29123 . . . . 5
34 eqeq2 2456 . . . . . 6
3534biimpd 200 . . . . 5
3631, 33, 35e11 29184 . . . 4
37 dffv4 5776 . . . . . 6
3837ax-gen 1556 . . . . 5
39 csbeq2g 29031 . . . . 5
401, 38, 39e10 29190 . . . 4
41 eqeq2 2456 . . . . 5
4241biimpd 200 . . . 4
4336, 40, 42e11 29184 . . 3
44 dffv4 5776 . . 3
45 eqeq2 2456 . . . 4
4645biimprcd 218 . . 3
4743, 44, 46e10 29190 . 2
4847in1 29057 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  A.wal 1550  =wceq 1654  e.wcel 1728  {cab 2433  [.wsbc 3174  [_csb 3274  {csn 3845  U.cuni 4047  "cima 4926  `cfv 5505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1955  ax-ext 2428  ax-sep 4368  ax-nul 4376  ax-pow 4420  ax-pr 4446
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-fal 1330  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2296  df-mo 2297  df-clab 2434  df-cleq 2440  df-clel 2443  df-nfc 2572  df-ne 2612  df-ral 2721  df-rex 2722  df-rab 2725  df-v 2971  df-sbc 3175  df-csb 3275  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-nul 3621  df-if 3770  df-sn 3851  df-pr 3852  df-op 3854  df-uni 4048  df-br 4248  df-opab 4306  df-xp 4929  df-cnv 4931  df-dm 4933  df-rn 4934  df-res 4935  df-ima 4936  df-iota 5468  df-fv 5513  df-vd1 29056
  Copyright terms: Public domain W3C validator