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

Theorem csbresgVD 34077
Description: Virtual deduction proof of csbresgOLD 34001. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbresgOLD 34001 is csbresgVD 34077 without virtual deductions and was automatically derived from csbresgVD 34077.
1::  |-  (. A  e.  V  ->.  A  e.  V ).
2:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ _V  =  _V ).
3:2:  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V )  =  ( [_ A  /  x ]_ C  X.  _V ) ).
4:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V ) ).
5:3,4:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  _V ) ).
6:5:  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V ) )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V ) ) ).
7:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  ( [_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V ) ) ).
8:6,7:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V ) ) ).
9::  |-  ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
10:9:  |-  A. x ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
11:1,10:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) ) ).
12:8,11:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  (  [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V ) ) ).
13::  |-  ( [_ A  /  x ]_ B  |`  [_ A  /  x ]_ C )  =  (  [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V ) )
14:12,13:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  (  [_ A  /  x ]_ B  |`  [_ A  /  x ]_ C ) ).
qed:14:  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( B  |`  C )  =  (  [_ A  /  x ]_ B  |`  [_ A  /  x ]_ C ) )
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbresgVD  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( B  |`  C )  =  (
[_ A  /  x ]_ B  |`  [_ A  /  x ]_ C ) )

Proof of Theorem csbresgVD
StepHypRef Expression
1 idn1 33726 . . . . . . . . 9  |-  (. A  e.  V  ->.  A  e.  V ).
2 csbconstg 3374 . . . . . . . . 9  |-  ( A  e.  V  ->  [_ A  /  x ]_ _V  =  _V )
31, 2e1a 33788 . . . . . . . 8  |-  (. A  e.  V  ->.  [_ A  /  x ]_ _V  =  _V ).
4 xpeq2 4941 . . . . . . . 8  |-  ( [_ A  /  x ]_ _V  =  _V  ->  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V )  =  (
[_ A  /  x ]_ C  X.  _V )
)
53, 4e1a 33788 . . . . . . 7  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V )  =  ( [_ A  /  x ]_ C  X.  _V ) ).
6 csbxpgOLD 33999 . . . . . . . 8  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V ) )
71, 6e1a 33788 . . . . . . 7  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V ) ).
8 eqeq2 2407 . . . . . . . 8  |-  ( (
[_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V )  =  ( [_ A  /  x ]_ C  X.  _V )  ->  ( [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V ) 
<-> 
[_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  _V ) ) )
98biimpd 207 . . . . . . 7  |-  ( (
[_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V )  =  ( [_ A  /  x ]_ C  X.  _V )  ->  ( [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V )  ->  [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  _V ) ) )
105, 7, 9e11 33849 . . . . . 6  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  _V ) ).
11 ineq2 3621 . . . . . 6  |-  ( [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  _V )  ->  ( [_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V )
)  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V ) ) )
1210, 11e1a 33788 . . . . 5  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V )
)  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V ) ) ).
13 csbingOLD 34000 . . . . . 6  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  (
[_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V ) ) )
141, 13e1a 33788 . . . . 5  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  ( [_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V )
) ).
15 eqeq2 2407 . . . . . 6  |-  ( (
[_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V ) )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
)  ->  ( [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  (
[_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V ) )  <->  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
) ) )
1615biimpd 207 . . . . 5  |-  ( (
[_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V ) )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
)  ->  ( [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  (
[_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V ) )  ->  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
) ) )
1712, 14, 16e11 33849 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
) ).
18 df-res 4938 . . . . . 6  |-  ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
1918ax-gen 1633 . . . . 5  |-  A. x
( B  |`  C )  =  ( B  i^i  ( C  X.  _V )
)
20 csbeq2gOLD 33697 . . . . 5  |-  ( A  e.  V  ->  ( A. x ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )  ->  [_ A  /  x ]_ ( B  |`  C )  =  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V )
) ) )
211, 19, 20e10 33855 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V )
) ).
22 eqeq2 2407 . . . . 5  |-  ( [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  (
[_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
)  ->  ( [_ A  /  x ]_ ( B  |`  C )  = 
[_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  <->  [_ A  /  x ]_ ( B  |`  C )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
) ) )
2322biimpd 207 . . . 4  |-  ( [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  (
[_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
)  ->  ( [_ A  /  x ]_ ( B  |`  C )  = 
[_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  ->  [_ A  /  x ]_ ( B  |`  C )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
) ) )
2417, 21, 23e11 33849 . . 3  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
) ).
25 df-res 4938 . . 3  |-  ( [_ A  /  x ]_ B  |` 
[_ A  /  x ]_ C )  =  (
[_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
)
26 eqeq2 2407 . . . 4  |-  ( (
[_ A  /  x ]_ B  |`  [_ A  /  x ]_ C )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
)  ->  ( [_ A  /  x ]_ ( B  |`  C )  =  ( [_ A  /  x ]_ B  |`  [_ A  /  x ]_ C )  <->  [_ A  /  x ]_ ( B  |`  C )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
) ) )
2726biimprcd 225 . . 3  |-  ( [_ A  /  x ]_ ( B  |`  C )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
)  ->  ( ( [_ A  /  x ]_ B  |`  [_ A  /  x ]_ C )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
)  ->  [_ A  /  x ]_ ( B  |`  C )  =  (
[_ A  /  x ]_ B  |`  [_ A  /  x ]_ C ) ) )
2824, 25, 27e10 33855 . 2  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  ( [_ A  /  x ]_ B  |`  [_ A  /  x ]_ C ) ).
2928in1 33723 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( B  |`  C )  =  (
[_ A  /  x ]_ B  |`  [_ A  /  x ]_ C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1397    = wceq 1399    e. wcel 1836   _Vcvv 3047   [_csb 3361    i^i cin 3401    X. cxp 4924    |` cres 4928
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-in 3409  df-opab 4439  df-xp 4932  df-res 4938  df-vd1 33722
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator