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

Theorem csbsngVD 30475
Description: Virtual deduction proof of csbsng 3967. 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 3967 is csbsngVD 30475 without virtual deductions and was automatically derived from csbsngVD 30475.
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 30133 . . . . . . . . 9
2 sbceqg 3712 . . . . . . . . 9
31, 2e1_ 30196 . . . . . . . 8
4 csbconstg 3338 . . . . . . . . . 10
51, 4e1_ 30196 . . . . . . . . 9
6 eqeq1 2495 . . . . . . . . 9
75, 6e1_ 30196 . . . . . . . 8
8 bibi1 319 . . . . . . . . 9
98biimprd 216 . . . . . . . 8
103, 7, 9e11 30257 . . . . . . 7
1110gen11 30185 . . . . . 6
12 abbi 2599 . . . . . . 7
1312biimpi 188 . . . . . 6
1411, 13e1_ 30196 . . . . 5
15 csbabgOLD 3743 . . . . . . 7
1615eqcomd 2494 . . . . . 6
171, 16e1_ 30196 . . . . 5
18 eqeq1 2495 . . . . . 6
1918biimpcd 217 . . . . 5
2014, 17, 19e11 30257 . . . 4
21 df-sn 3915 . . . . . 6
2221ax-gen 1570 . . . . 5
23 csbeq2gOLD 30104 . . . . 5
241, 22, 23e10 30263 . . . 4
25 eqeq2 2498 . . . . 5
2625biimpd 200 . . . 4
2720, 24, 26e11 30257 . . 3
28 df-sn 3915 . . 3
29 eqeq2 2498 . . . 4
3029biimprcd 218 . . 3
3127, 28, 30e10 30263 . 2
3231in1 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
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-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-v 3017  df-sbc 3225  df-csb 3326  df-sn 3915  df-vd1 30129
  Copyright terms: Public domain W3C validator