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

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

Proof of Theorem csbresgVD
StepHypRef Expression
1 idn1 29060 . . . . . . . . 9
2 csbconstg 3286 . . . . . . . . 9
31, 2e1_ 29123 . . . . . . . 8
4 xpeq2 4938 . . . . . . . 8
53, 4e1_ 29123 . . . . . . 7
6 csbxpgOLD 5002 . . . . . . . 8
71, 6e1_ 29123 . . . . . . 7
8 eqeq2 2456 . . . . . . . 8
98biimpd 200 . . . . . . 7
105, 7, 9e11 29184 . . . . . 6
11 ineq2 3529 . . . . . 6
1210, 11e1_ 29123 . . . . 5
13 csbingOLD 3692 . . . . . 6
141, 13e1_ 29123 . . . . 5
15 eqeq2 2456 . . . . . 6
1615biimpd 200 . . . . 5
1712, 14, 16e11 29184 . . . 4
18 df-res 4935 . . . . . 6
1918ax-gen 1556 . . . . 5
20 csbeq2g 29031 . . . . 5
211, 19, 20e10 29190 . . . 4
22 eqeq2 2456 . . . . 5
2322biimpd 200 . . . 4
2417, 21, 23e11 29184 . . 3
25 df-res 4935 . . 3
26 eqeq2 2456 . . . 4
2726biimprcd 218 . . 3
2824, 25, 27e10 29190 . 2
2928in1 29057 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  A.wal 1550  =wceq 1654  e.wcel 1728   cvv 2969  [_csb 3274  i^icin 3312  X.cxp 4921  |`cres 4925
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-3an 939  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-rab 2725  df-v 2971  df-sbc 3175  df-csb 3275  df-in 3320  df-opab 4306  df-xp 4929  df-res 4935  df-vd1 29056
  Copyright terms: Public domain W3C validator