Theorem csbresgVD 37302

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

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

Step	Hyp	Ref	Expression
1		idn1 36955	. . . . . . . . 9 |- (. A e. V ->. A e. V ).
2		csbconstg 3378	. . . . . . . . 9 |- ( A e. V -> [_ A / x ]_ _V = _V )
3	1, 2	e1a 37017	. . . . . . . 8 |- (. A e. V ->. [_ A / x ]_ _V = _V ).
4		xpeq2 4852	. . . . . . . 8 |- ( [_ A / x ]_ _V = _V -> ( [_ A / x ]_ C X. [_ A / x ]_ _V ) = ( [_ A / x ]_ C X. _V ) )
5	3, 4	e1a 37017	. . . . . . 7 |- (. A e. V ->. ( [_ A / x ]_ C X. [_ A / x ]_ _V ) = ( [_ A / x ]_ C X. _V ) ).
6		csbxpgOLD 37224	. . . . . . . 8 |- ( A e. V -> [_ A / x ]_ ( C X. _V ) = ( [_ A / x ]_ C X. [_ A / x ]_ _V ) )
7	1, 6	e1a 37017	. . . . . . 7 |- (. A e. V ->. [_ A / x ]_ ( C X. _V ) = ( [_ A / x ]_ C X. [_ A / x ]_ _V ) ).
8		eqeq2 2464	. . . . . . . 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 ) ) )
9	8	biimpd 211	. . . . . . 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 ) ) )
10	5, 7, 9	e11 37078	. . . . . 6 |- (. A e. V ->. [_ A / x ]_ ( C X. _V ) = ( [_ A / x ]_ C X. _V ) ).
11		ineq2 3630	. . . . . 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 ) ) )
12	10, 11	e1a 37017	. . . . 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 37225	. . . . . 6 |- ( A e. V -> [_ A / x ]_ ( B i^i ( C X. _V ) ) = ( [_ A / x ]_ B i^i [_ A / x ]_ ( C X. _V ) ) )
14	1, 13	e1a 37017	. . . . 5 |- (. A e. V ->. [_ A / x ]_ ( B i^i ( C X. _V ) ) = ( [_ A / x ]_ B i^i [_ A / x ]_ ( C X. _V ) ) ).
15		eqeq2 2464	. . . . . 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 ) ) ) )
16	15	biimpd 211	. . . . 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 ) ) ) )
17	12, 14, 16	e11 37078	. . . 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 4849	. . . . . 6 |- ( B |` C ) = ( B i^i ( C X. _V ) )
19	18	ax-gen 1671	. . . . 5 |- A. x ( B |` C ) = ( B i^i ( C X. _V ) )
20		csbeq2gOLD 36927	. . . . 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 ) ) ) )
21	1, 19, 20	e10 37084	. . . 4 |- (. A e. V ->. [_ A / x ]_ ( B |` C ) = [_ A / x ]_ ( B i^i ( C X. _V ) ) ).
22		eqeq2 2464	. . . . 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 ) ) ) )
23	22	biimpd 211	. . . 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 ) ) ) )
24	17, 21, 23	e11 37078	. . 3 |- (. A e. V ->. [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B i^i ( [_ A / x ]_ C X. _V ) ) ).
25		df-res 4849	. . 3 |- ( [_ A / x ]_ B |` [_ A / x ]_ C ) = ( [_ A / x ]_ B i^i ( [_ A / x ]_ C X. _V ) )
26		eqeq2 2464	. . . 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 ) ) ) )
27	26	biimprcd 229	. . 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 ) ) )
28	24, 25, 27	e10 37084	. 2 |- (. A e. V ->. [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C ) ).
29	28	in1 36952	1 |- ( A e. V -> [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C ) )

Syntax hints:   -> wi 4   A.wal 1444   = wceq 1446   e. wcel 1889   _Vcvv 3047   [_csb 3365   i^i cin 3405   X. cxp 4835   |` cres 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-in 3413  df-opab 4465  df-xp 4843  df-res 4849  df-vd1 36951

This theorem is referenced by: (None)