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

Theorem csbsngVD 29402
Description: Virtual deduction proof of csbsng 3899. 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 3899 is csbsngVD 29402 without virtual deductions and was automatically derived from csbsngVD 29402.
1:: |-(. e. ->. e. ).
2:1: |-(. e. ->.([. ]. = <->[_ ]_ =[_ ]_ )).
3:1: |-(. e. ->.[_ ]_ = ).
4:3: |-(. e. ->.([_ ]_ =[_ ]_ <-> =[_ ]_ )).
5:2,4: |-(. e. ->.([. ]. = <-> =[_ ]_ )).
6:5: |-(. e. ->.A. ([. ]. = <-> =[_ ]_ )).
7:6: |-(. e. ->.{ |[. ]. = }={ | =[_ ]_ }).
8:1: |-(. e. ->.{ |[. ]. = }=[_ ]_{ | = }).
9:7,8: |-(. e. ->.[_ ]_{ | = }={ | =[_ ]_ }).
10:: |-{ }={ | = }
11:10: |-A. { }={ | = }
12:1,11: |-(. e. ->.[_ ]_{ }=[_ ]_{ | = }).
13:9,12: |-(. e. ->.[_ ]_{ }={ | =[_ ]_ }).
14:: |-{[_ ]_ }={ | =[_ ]_ }
15:13,14: |-(. e. ->.[_ ]_{ }={ [_ ]_ }).
qed:15: |-( e. ->[_ ]_{ }={[_ ]_ })
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbsngVD

Proof of Theorem csbsngVD
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 idn1 29060 . . . . . . . . 9
2 sbceqg 3659 . . . . . . . . 9
31, 2e1_ 29123 . . . . . . . 8
4 csbconstg 3286 . . . . . . . . . 10
51, 4e1_ 29123 . . . . . . . . 9
6 eqeq1 2453 . . . . . . . . 9
75, 6e1_ 29123 . . . . . . . 8
8 bibi1 319 . . . . . . . . 9
98biimprd 216 . . . . . . . 8
103, 7, 9e11 29184 . . . . . . 7
1110gen11 29112 . . . . . 6
12 abbi 2557 . . . . . . 7
1312biimpi 188 . . . . . 6
1411, 13e1_ 29123 . . . . 5
15 csbabgOLD 3690 . . . . . . 7
1615eqcomd 2452 . . . . . 6
171, 16e1_ 29123 . . . . 5
18 eqeq1 2453 . . . . . 6
1918biimpcd 217 . . . . 5
2014, 17, 19e11 29184 . . . 4
21 df-sn 3851 . . . . . 6
2221ax-gen 1556 . . . . 5
23 csbeq2g 29031 . . . . 5
241, 22, 23e10 29190 . . . 4
25 eqeq2 2456 . . . . 5
2625biimpd 200 . . . 4
2720, 24, 26e11 29184 . . 3
28 df-sn 3851 . . 3
29 eqeq2 2456 . . . 4
3029biimprcd 218 . . 3
3127, 28, 30e10 29190 . 2
3231in1 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
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-6 1747  ax-7 1752  ax-11 1764  ax-12 1955  ax-ext 2428
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2434  df-cleq 2440  df-clel 2443  df-nfc 2572  df-v 2971  df-sbc 3175  df-csb 3275  df-sn 3851  df-vd1 29056
  Copyright terms: Public domain W3C validator