Metamath Proof Explorer

Theorem csbresgVD

Description: Virtual deduction proof of csbres . 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. csbres is csbresgVD without virtual deductions and was automatically derived from csbresgVD .

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.)

Ref Expression
Assertion csbresgVD 
|- ( A e. V -> [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C ) )

Proof

Step Hyp Ref Expression
1 idn1 
 |-  (. A e. V ->. A e. V ).
2 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ _V = _V )
3 1 2 e1a 
 |-  (. A e. V ->. [_ A / x ]_ _V = _V ).
4 xpeq2 
 |-  ( [_ A / x ]_ _V = _V -> ( [_ A / x ]_ C X. [_ A / x ]_ _V ) = ( [_ A / x ]_ C X. _V ) )
5 3 4 e1a 
 |-  (. A e. V ->. ( [_ A / x ]_ C X. [_ A / x ]_ _V ) = ( [_ A / x ]_ C X. _V ) ).
6 csbxp 
 |-  [_ A / x ]_ ( C X. _V ) = ( [_ A / x ]_ C X. [_ A / x ]_ _V )
7 6 a1i 
 |-  ( A e. V -> [_ A / x ]_ ( C X. _V ) = ( [_ A / x ]_ C X. [_ A / x ]_ _V ) )
8 1 7 e1a 
 |-  (. A e. V ->. [_ A / x ]_ ( C X. _V ) = ( [_ A / x ]_ C X. [_ A / x ]_ _V ) ).
9 eqeq2 
 |-  ( ( [_ 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 ) ) )
10 9 biimpd 
 |-  ( ( [_ 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 ) ) )
11 5 8 10 e11 
 |-  (. A e. V ->. [_ A / x ]_ ( C X. _V ) = ( [_ A / x ]_ C X. _V ) ).
12 ineq2 
 |-  ( [_ 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 ) ) )
13 11 12 e1a 
 |-  (. A e. V ->. ( [_ A / x ]_ B i^i [_ A / x ]_ ( C X. _V ) ) = ( [_ A / x ]_ B i^i ( [_ A / x ]_ C X. _V ) ) ).
14 csbin 
 |-  [_ A / x ]_ ( B i^i ( C X. _V ) ) = ( [_ A / x ]_ B i^i [_ A / x ]_ ( C X. _V ) )
15 14 a1i 
 |-  ( A e. V -> [_ A / x ]_ ( B i^i ( C X. _V ) ) = ( [_ A / x ]_ B i^i [_ A / x ]_ ( C X. _V ) ) )
16 1 15 e1a 
 |-  (. A e. V ->. [_ A / x ]_ ( B i^i ( C X. _V ) ) = ( [_ A / x ]_ B i^i [_ A / x ]_ ( C X. _V ) ) ).
17 eqeq2 
 |-  ( ( [_ 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 ) ) ) )
18 17 biimpd 
 |-  ( ( [_ 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 ) ) ) )
19 13 16 18 e11 
 |-  (. A e. V ->. [_ A / x ]_ ( B i^i ( C X. _V ) ) = ( [_ A / x ]_ B i^i ( [_ A / x ]_ C X. _V ) ) ).
20 df-res 
 |-  ( B |` C ) = ( B i^i ( C X. _V ) )
21 20 ax-gen 
 |-  A. x ( B |` C ) = ( B i^i ( C X. _V ) )
22 csbeq2 
 |-  ( A. x ( B |` C ) = ( B i^i ( C X. _V ) ) -> [_ A / x ]_ ( B |` C ) = [_ A / x ]_ ( B i^i ( C X. _V ) ) )
23 22 a1i 
 |-  ( 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 ) ) ) )
24 1 21 23 e10 
 |-  (. A e. V ->. [_ A / x ]_ ( B |` C ) = [_ A / x ]_ ( B i^i ( C X. _V ) ) ).
25 eqeq2 
 |-  ( [_ 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 ) ) ) )
26 25 biimpd 
 |-  ( [_ 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 ) ) ) )
27 19 24 26 e11 
 |-  (. A e. V ->. [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B i^i ( [_ A / x ]_ C X. _V ) ) ).
28 df-res 
 |-  ( [_ A / x ]_ B |` [_ A / x ]_ C ) = ( [_ A / x ]_ B i^i ( [_ A / x ]_ C X. _V ) )
29 eqeq2 
 |-  ( ( [_ 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 ) ) ) )
30 29 biimprcd 
 |-  ( [_ 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 ) ) )
31 27 28 30 e10 
 |-  (. A e. V ->. [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C ) ).
32 31 in1 
 |-  ( A e. V -> [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C ) )