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

Theorem csbsngVD 30198
Description: Virtual deduction proof of csbsng 3952. 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 3952 is csbsngVD 30198 without virtual deductions and was automatically derived from csbsngVD 30198.
1:: |-(.Ae. ->.Ae. ).
2:1: |-(.Ae. ->.([.A ]. =B <->[_A ]_ =[_A ]_B)).
3:1: |-(.Ae. ->.[_A ]_ = ).
4:3: |-(.Ae. ->.([_A ]_ =[_A ]_B<-> =[_A ]_B)).
5:2,4: |-(.Ae. ->.([.A ]. =B <-> =[_A ]_B)).
6:5: |-(.Ae. ->.A. ([.A ]. =B<-> =[_A ]_B)).
7:6: |-(.Ae. ->.{ |[.A ]. = B}={ | =[_A ]_B}).
8:1: |-(.Ae. ->.{ |[.A ]. = B}=[_A ]_{ | =B}).
9:7,8: |-(.Ae. ->.[_A ]_{ | =B}={ | =[_A ]_B}).
10:: |-{B}={ | =B}
11:10: |-A. {B}={ | =B}
12:1,11: |-(.Ae. ->.[_A ]_{B}=[_ A ]_{ | =B}).
13:9,12: |-(.Ae. ->.[_A ]_{B}={ | =[_A ]_B}).
14:: |-{[_A ]_B}={ | =[_A ]_B}
15:13,14: |-(.Ae. ->.[_A ]_{B}={ [_A ]_B}).
qed:15: |-(Ae. ->[_A ]_{B}={[_ A ]_B})
(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 29856 . . . . . . . . 9
2 sbceqg 3699 . . . . . . . . 9
31, 2e1_ 29919 . . . . . . . 8
4 csbconstg 3326 . . . . . . . . . 10
51, 4e1_ 29919 . . . . . . . . 9
6 eqeq1 2487 . . . . . . . . 9
75, 6e1_ 29919 . . . . . . . 8
8 bibi1 319 . . . . . . . . 9
98biimprd 216 . . . . . . . 8
103, 7, 9e11 29980 . . . . . . 7
1110gen11 29908 . . . . . 6
12 abbi 2591 . . . . . . 7
1312biimpi 188 . . . . . 6
1411, 13e1_ 29919 . . . . 5
15 csbabgOLD 3730 . . . . . . 7
1615eqcomd 2486 . . . . . 6
171, 16e1_ 29919 . . . . 5
18 eqeq1 2487 . . . . . 6
1918biimpcd 217 . . . . 5
2014, 17, 19e11 29980 . . . 4
21 df-sn 3900 . . . . . 6
2221ax-gen 1562 . . . . 5
23 csbeq2gOLD 29827 . . . . 5
241, 22, 23e10 29986 . . . 4
25 eqeq2 2490 . . . . 5
2625biimpd 200 . . . 4
2720, 24, 26e11 29980 . . 3
28 df-sn 3900 . . 3
29 eqeq2 2490 . . . 4
3029biimprcd 218 . . 3
3127, 28, 30e10 29986 . 2
3231in1 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
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-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-v 3008  df-sbc 3213  df-csb 3314  df-sn 3900  df-vd1 29852
  Copyright terms: Public domain W3C validator