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

Theorem csbresgVD 33423
Description: Virtual deduction proof of csbresgOLD 5264. 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 5264 is csbresgVD 33423 without virtual deductions and was automatically derived from csbresgVD 33423.
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 33079 . . . . . . . . 9  |-  (. A  e.  V  ->.  A  e.  V ).
2 csbconstg 3431 . . . . . . . . 9  |-  ( A  e.  V  ->  [_ A  /  x ]_ _V  =  _V )
31, 2e1a 33141 . . . . . . . 8  |-  (. A  e.  V  ->.  [_ A  /  x ]_ _V  =  _V ).
4 xpeq2 5001 . . . . . . . 8  |-  ( [_ A  /  x ]_ _V  =  _V  ->  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V )  =  (
[_ A  /  x ]_ C  X.  _V )
)
53, 4e1a 33141 . . . . . . 7  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V )  =  ( [_ A  /  x ]_ C  X.  _V ) ).
6 csbxpgOLD 5069 . . . . . . . 8  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V ) )
71, 6e1a 33141 . . . . . . 7  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V ) ).
8 eqeq2 2456 . . . . . . . 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 33202 . . . . . 6  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  _V ) ).
11 ineq2 3677 . . . . . 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 33141 . . . . 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 3844 . . . . . 6  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  (
[_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V ) ) )
141, 13e1a 33141 . . . . 5  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  ( [_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V )
) ).
15 eqeq2 2456 . . . . . 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 33202 . . . 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 4998 . . . . . 6  |-  ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
1918ax-gen 1603 . . . . 5  |-  A. x
( B  |`  C )  =  ( B  i^i  ( C  X.  _V )
)
20 csbeq2gOLD 33050 . . . . 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 33208 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V )
) ).
22 eqeq2 2456 . . . . 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 33202 . . 3  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
) ).
25 df-res 4998 . . 3  |-  ( [_ A  /  x ]_ B  |` 
[_ A  /  x ]_ C )  =  (
[_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
)
26 eqeq2 2456 . . . 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 33208 . 2  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  ( [_ A  /  x ]_ B  |`  [_ A  /  x ]_ C ) ).
2928in1 33076 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 1379    = wceq 1381    e. wcel 1802   _Vcvv 3093   [_csb 3418    i^i cin 3458    X. cxp 4984    |` cres 4988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3419  df-in 3466  df-opab 4493  df-xp 4992  df-res 4998  df-vd1 33075
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator