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

Theorem csbresgVD 30200
Description: Virtual deduction proof of csbresgOLD 5118. 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 5118 is csbresgVD 30200 without virtual deductions and was automatically derived from csbresgVD 30200.
1:: |-(.Ae. ->.Ae. ).
2:1: |-(.Ae. ->.[_A ]_ = ).
3:2: |-(.Ae. ->.([_A ]_ X.[_A ]_ )=([_A ]_ X. )).
4:1: |-(.Ae. ->.[_A ]_( X. )= ([_A ]_ X.[_A ]_ )).
5:3,4: |-(.Ae. ->.[_A ]_( X. )= ([_A ]_ X. )).
6:5: |-(.Ae. ->.([_A ]_Bi^i[_A ]_( X. ))= ([_A ]_Bi^i([_A ]_ X. ))).
7:1: |-(.Ae. ->.[_A ]_(Bi^i( X. ))=([_A ]_Bi^i[_A ]_( X. ))).
8:6,7: |-(.Ae. ->.[_A ]_(Bi^i( X. ))=([_A ]_Bi^i([_A ]_ X. ))).
9:: |-(B|` )=(Bi^i( X. ))
10:9: |-A. (B|` )=(Bi^i( X. ))
11:1,10: |-(.Ae. ->.[_A ]_(B|` )= [_A ]_(Bi^i( X. ))).
12:8,11: |-(.Ae. ->.[_A ]_(B|` ) =( [_A ]_Bi^i([_A ]_ X. ))).
13:: |-([_A ]_B|`[_A ]_ )=( [_A ]_Bi^i([_A ]_ X. ))
14:12,13: |-(.Ae. ->.[_A ]_(B|` )= ( [_A ]_B|`[_A ]_ )).
qed:14: |-(Ae. ->[_A ]_(B|` )=( [_A ]_B|`[_A ]_ ))
(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 29856 . . . . . . . . 9
2 csbconstg 3326 . . . . . . . . 9
31, 2e1_ 29919 . . . . . . . 8
4 xpeq2 4859 . . . . . . . 8
53, 4e1_ 29919 . . . . . . 7
6 csbxpgOLD 4923 . . . . . . . 8
71, 6e1_ 29919 . . . . . . 7
8 eqeq2 2490 . . . . . . . 8
98biimpd 200 . . . . . . 7
105, 7, 9e11 29980 . . . . . 6
11 ineq2 3569 . . . . . 6
1210, 11e1_ 29919 . . . . 5
13 csbingOLD 3735 . . . . . 6
141, 13e1_ 29919 . . . . 5
15 eqeq2 2490 . . . . . 6
1615biimpd 200 . . . . 5
1712, 14, 16e11 29980 . . . 4
18 df-res 4856 . . . . . 6
1918ax-gen 1562 . . . . 5
20 csbeq2gOLD 29827 . . . . 5
211, 19, 20e10 29986 . . . 4
22 eqeq2 2490 . . . . 5
2322biimpd 200 . . . 4
2417, 21, 23e11 29980 . . 3
25 df-res 4856 . . 3
26 eqeq2 2490 . . . 4
2726biimprcd 218 . . 3
2824, 25, 27e10 29986 . 2
2928in1 29853 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  A.wal 1556  =wceq 1662  e.wcel 1724   cvv 3006  [_csb 3313  i^icin 3352  X.cxp 4842  |`cres 4846
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-3an 941  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-rab 2760  df-v 3008  df-sbc 3213  df-csb 3314  df-in 3360  df-opab 4361  df-xp 4850  df-res 4856  df-vd1 29852
  Copyright terms: Public domain W3C validator