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

Theorem csbresgVD 28671
Description: Virtual deduction proof of csbresg 4958. 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. csbresg 4958 is csbresgVD 28671 without virtual deductions and was automatically derived from csbresgVD 28671.
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 28342 . . . . . . . . 9  |-  (. A  e.  V  ->.  A  e.  V ).
2 csbconstg 3095 . . . . . . . . 9  |-  ( A  e.  V  ->  [_ A  /  x ]_ _V  =  _V )
31, 2e1_ 28399 . . . . . . . 8  |-  (. A  e.  V  ->.  [_ A  /  x ]_ _V  =  _V ).
4 xpeq2 4704 . . . . . . . 8  |-  ( [_ A  /  x ]_ _V  =  _V  ->  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V )  =  (
[_ A  /  x ]_ C  X.  _V )
)
53, 4e1_ 28399 . . . . . . 7  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V )  =  ( [_ A  /  x ]_ C  X.  _V ) ).
6 csbxpg 4716 . . . . . . . 8  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V ) )
71, 6e1_ 28399 . . . . . . 7  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V ) ).
8 eqeq2 2292 . . . . . . . 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 198 . . . . . . 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 28460 . . . . . 6  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  _V ) ).
11 ineq2 3364 . . . . . 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, 11e1_ 28399 . . . . 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 csbing 3376 . . . . . 6  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  (
[_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V ) ) )
141, 13e1_ 28399 . . . . 5  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  ( [_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V )
) ).
15 eqeq2 2292 . . . . . 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 198 . . . . 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 28460 . . . 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 4701 . . . . . 6  |-  ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
1918ax-gen 1533 . . . . 5  |-  A. x
( B  |`  C )  =  ( B  i^i  ( C  X.  _V )
)
20 csbeq2g 28315 . . . . 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 28467 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V )
) ).
22 eqeq2 2292 . . . . 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 198 . . . 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 28460 . . 3  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
) ).
25 df-res 4701 . . 3  |-  ( [_ A  /  x ]_ B  |` 
[_ A  /  x ]_ C )  =  (
[_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V )
)
26 eqeq2 2292 . . . 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 216 . . 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 28467 . 2  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  ( [_ A  /  x ]_ B  |`  [_ A  /  x ]_ C ) ).
2928in1 28339 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( B  |`  C )  =  (
[_ A  /  x ]_ B  |`  [_ A  /  x ]_ C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527    = wceq 1623    e. wcel 1684   _Vcvv 2788   [_csb 3081    i^i cin 3151    X. cxp 4687    |` cres 4691
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-in 3159  df-opab 4078  df-xp 4695  df-res 4701  df-vd1 28338
  Copyright terms: Public domain W3C validator