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

Theorem csbfv12gALTVD 30204
Description: Virtual deduction proof of csbfv12gALTOLD 30127. 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 30127 is csbfv12gALTVD 30204 without virtual deductions and was automatically derived from csbfv12gALTVD 30204.
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 29856 . . . . . . . . . . 11
2 sbceqg 3699 . . . . . . . . . . 11
31, 2e1_ 29919 . . . . . . . . . 10
4 csbima12gOLD 5189 . . . . . . . . . . . . 13
51, 4e1_ 29919 . . . . . . . . . . . 12
6 csbsng 3952 . . . . . . . . . . . . . 14
71, 6e1_ 29919 . . . . . . . . . . . . 13
8 imaeq2 5167 . . . . . . . . . . . . 13
97, 8e1_ 29919 . . . . . . . . . . . 12
10 eqeq1 2487 . . . . . . . . . . . . 13
1110biimprd 216 . . . . . . . . . . . 12
125, 9, 11e11 29980 . . . . . . . . . . 11
13 csbconstg 3326 . . . . . . . . . . . 12
141, 13e1_ 29919 . . . . . . . . . . 11
15 eqeq12 2493 . . . . . . . . . . . 12
1615ex 425 . . . . . . . . . . 11
1712, 14, 16e11 29980 . . . . . . . . . 10
18 bibi1 319 . . . . . . . . . . 11
1918biimprd 216 . . . . . . . . . 10
203, 17, 19e11 29980 . . . . . . . . 9
2120gen11 29908 . . . . . . . 8
22 abbi 2591 . . . . . . . . 9
2322biimpi 188 . . . . . . . 8
2421, 23e1_ 29919 . . . . . . 7
25 csbabgOLD 3730 . . . . . . . 8
261, 25e1_ 29919 . . . . . . 7
27 eqeq2 2490 . . . . . . . 8
2827biimpd 200 . . . . . . 7
2924, 26, 28e11 29980 . . . . . 6
30 unieq 4109 . . . . . 6
3129, 30e1_ 29919 . . . . 5
32 csbunigOLD 4130 . . . . . 6
331, 32e1_ 29919 . . . . 5
34 eqeq2 2490 . . . . . 6
3534biimpd 200 . . . . 5
3631, 33, 35e11 29980 . . . 4
37 dffv4 5682 . . . . . 6
3837ax-gen 1562 . . . . 5
39 csbeq2gOLD 29827 . . . . 5
401, 38, 39e10 29986 . . . 4
41 eqeq2 2490 . . . . 5
4241biimpd 200 . . . 4
4336, 40, 42e11 29980 . . 3
44 dffv4 5682 . . 3
45 eqeq2 2490 . . . 4
4645biimprcd 218 . . 3
4743, 44, 46e10 29986 . 2
4847in1 29853 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  A.wal 1556  =wceq 1662  e.wcel 1724  {cab 2467  [.wsbc 3212  [_csb 3313  {csn 3894  U.cuni 4101  "cima 4847  `cfv 5417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-8 1726  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pow 4477  ax-pr 4538
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1337  df-fal 1338  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2309  df-mo 2310  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3008  df-sbc 3213  df-csb 3314  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-nul 3661  df-if 3813  df-sn 3900  df-pr 3901  df-op 3903  df-uni 4102  df-br 4303  df-opab 4361  df-xp 4850  df-cnv 4852  df-dm 4854  df-rn 4855  df-res 4856  df-ima 4857  df-iota 5380  df-fv 5425  df-vd1 29852
  Copyright terms: Public domain W3C validator