Theorem csbfv12gALTOLD 37254

Description: Move class substitution in and out of a function value. The proof is derived from the virtual deduction proof csbfv12gALTVD 37337. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 20-Aug-2018. Use csbfv12 5927 instead. (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
csbfv12gALTOLD	|- ( A e. C -> [_ A / x ]_ ( F ` B ) = ( [_ A / x ]_ F ` [_ A / x ]_ B ) )

Proof of Theorem csbfv12gALTOLD

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		csbunigOLD 37253	. . 3 |- ( A e. C -> [_ A / x ]_ U. { y | ( F " { B } ) = { y } } = U. [_ A / x ]_ { y | ( F " { B } ) = { y } } )
2		csbabgOLD 37252	. . . . 5 |- ( A e. C -> [_ A / x ]_ { y | ( F " { B } ) = { y } } = { y | [. A / x ]. ( F " { B } ) = { y } } )
3		sbceqg 3785	. . . . . . 7 |- ( A e. C -> ( [. A / x ]. ( F " { B } ) = { y } <-> [_ A / x ]_ ( F " { B } ) = [_ A / x ]_ { y } ) )
4		csbima12gOLD 5208	. . . . . . . . 9 |- ( A e. C -> [_ A / x ]_ ( F " { B } ) = ( [_ A / x ]_ F " [_ A / x ]_ { B } ) )
5		csbsng 4042	. . . . . . . . . 10 |- ( A e. C -> [_ A / x ]_ { B } = { [_ A / x ]_ B } )
6	5	imaeq2d 5190	. . . . . . . . 9 |- ( A e. C -> ( [_ A / x ]_ F " [_ A / x ]_ { B } ) = ( [_ A / x ]_ F " { [_ A / x ]_ B } ) )
7	4, 6	eqtrd 2496	. . . . . . . 8 |- ( A e. C -> [_ A / x ]_ ( F " { B } ) = ( [_ A / x ]_ F " { [_ A / x ]_ B } ) )
8		csbconstg 3388	. . . . . . . 8 |- ( A e. C -> [_ A / x ]_ { y } = { y } )
9	7, 8	eqeq12d 2477	. . . . . . 7 |- ( A e. C -> ( [_ A / x ]_ ( F " { B } ) = [_ A / x ]_ { y } <-> ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } ) )
10	3, 9	bitrd 261	. . . . . 6 |- ( A e. C -> ( [. A / x ]. ( F " { B } ) = { y } <-> ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } ) )
11	10	abbidv 2580	. . . . 5 |- ( A e. C -> { y | [. A / x ]. ( F " { B } ) = { y } } = { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } )
12	2, 11	eqtrd 2496	. . . 4 |- ( A e. C -> [_ A / x ]_ { y | ( F " { B } ) = { y } } = { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } )
13	12	unieqd 4222	. . 3 |- ( A e. C -> U. [_ A / x ]_ { y | ( F " { B } ) = { y } } = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } )
14	1, 13	eqtrd 2496	. 2 |- ( A e. C -> [_ A / x ]_ U. { y | ( F " { B } ) = { y } } = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } )
15		dffv4 5889	. . 3 |- ( F ` B ) = U. { y | ( F " { B } ) = { y } }
16	15	csbeq2i 3794	. 2 |- [_ A / x ]_ ( F ` B ) = [_ A / x ]_ U. { y | ( F " { B } ) = { y } }
17		dffv4 5889	. 2 |- ( [_ A / x ]_ F ` [_ A / x ]_ B ) = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } }
18	14, 16, 17	3eqtr4g 2521	1 |- ( A e. C -> [_ A / x ]_ ( F ` B ) = ( [_ A / x ]_ F ` [_ A / x ]_ B ) )

Syntax hints:   -> wi 4   = wceq 1455   e. wcel 1898   {cab 2448   [.wsbc 3279   [_csb 3375   {csn 3980   U.cuni 4212   "cima 4859   ` cfv 5605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-xp 4862  df-cnv 4864  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fv 5613

This theorem is referenced by: (None)