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

Step	Hyp	Ref	Expression
1		idn1 33079	. . . . . . . . 9 |- (. A e. V ->. A e. V ).
2		csbconstg 3431	. . . . . . . . 9 |- ( A e. V -> [_ A / x ]_ _V = _V )
3	1, 2	e1a 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 ) )
5	3, 4	e1a 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 ) )
7	1, 6	e1a 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 ) ) )
9	8	biimpd 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 ) ) )
10	5, 7, 9	e11 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 ) ) )
12	10, 11	e1a 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 ) ) )
14	1, 13	e1a 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 ) ) ) )
16	15	biimpd 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 ) ) ) )
17	12, 14, 16	e11 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 ) )
19	18	ax-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 ) ) ) )
21	1, 19, 20	e10 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 ) ) ) )
23	22	biimpd 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 ) ) ) )
24	17, 21, 23	e11 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 ) ) ) )
27	26	biimprcd 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 ) ) )
28	24, 25, 27	e10 33208	. 2 |- (. A e. V ->. [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C ) ).
29	28	in1 33076	1 |- ( A e. V -> [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C ) )

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)