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

Theorem csbresgVD 30477
Description: Virtual deduction proof of csbresgOLD 5136. 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 5136 is csbresgVD 30477 without virtual deductions and was automatically derived from csbresgVD 30477.
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 30133 . . . . . . . . 9
2 csbconstg 3338 . . . . . . . . 9
31, 2e1_ 30196 . . . . . . . 8
4 xpeq2 4877 . . . . . . . 8
53, 4e1_ 30196 . . . . . . 7
6 csbxpgOLD 4941 . . . . . . . 8
71, 6e1_ 30196 . . . . . . 7
8 eqeq2 2498 . . . . . . . 8
98biimpd 200 . . . . . . 7
105, 7, 9e11 30257 . . . . . 6
11 ineq2 3582 . . . . . 6
1210, 11e1_ 30196 . . . . 5
13 csbingOLD 3748 . . . . . 6
141, 13e1_ 30196 . . . . 5
15 eqeq2 2498 . . . . . 6
1615biimpd 200 . . . . 5
1712, 14, 16e11 30257 . . . 4
18 df-res 4874 . . . . . 6
1918ax-gen 1570 . . . . 5
20 csbeq2gOLD 30104 . . . . 5
211, 19, 20e10 30263 . . . 4
22 eqeq2 2498 . . . . 5
2322biimpd 200 . . . 4
2417, 21, 23e11 30257 . . 3
25 df-res 4874 . . 3
26 eqeq2 2498 . . . 4
2726biimprcd 218 . . 3
2824, 25, 27e10 30263 . 2
2928in1 30130 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  A.wal 1564  =wceq 1670  e.wcel 1732   cvv 3015  [_csb 3325  i^icin 3364  X.cxp 4860  |`cres 4864
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-3an 941  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-rab 2768  df-v 3017  df-sbc 3225  df-csb 3326  df-in 3372  df-opab 4377  df-xp 4868  df-res 4874  df-vd1 30129
  Copyright terms: Public domain W3C validator