Theorem csbrn

Description: Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012)

	Ref	Expression
Assertion	csbrn	|- [_ A / x ]_ ran B = ran [_ A / x ]_ B

Proof

Step	Hyp	Ref	Expression
1		csbima12	|- [_ A / x ]_ ( B " _V ) = ( [_ A / x ]_ B " [_ A / x ]_ _V )
2		csbconstg	|- ( A e. _V -> [_ A / x ]_ _V = _V )
3	2	imaeq2d	|- ( A e. _V -> ( [_ A / x ]_ B " [_ A / x ]_ _V ) = ( [_ A / x ]_ B " _V ) )
4		0ima	|- ( (/) " _V ) = (/)
5	4	eqcomi	|- (/) = ( (/) " _V )
6		csbprc	|- ( -. A e. _V -> [_ A / x ]_ B = (/) )
7	6	imaeq1d	|- ( -. A e. _V -> ( [_ A / x ]_ B " [_ A / x ]_ _V ) = ( (/) " [_ A / x ]_ _V ) )
8		0ima	|- ( (/) " [_ A / x ]_ _V ) = (/)
9	7 8	eqtrdi	|- ( -. A e. _V -> ( [_ A / x ]_ B " [_ A / x ]_ _V ) = (/) )
10	6	imaeq1d	|- ( -. A e. _V -> ( [_ A / x ]_ B " _V ) = ( (/) " _V ) )
11	5 9 10	3eqtr4a	|- ( -. A e. _V -> ( [_ A / x ]_ B " [_ A / x ]_ _V ) = ( [_ A / x ]_ B " _V ) )
12	3 11	pm2.61i	|- ( [_ A / x ]_ B " [_ A / x ]_ _V ) = ( [_ A / x ]_ B " _V )
13	1 12	eqtri	|- [_ A / x ]_ ( B " _V ) = ( [_ A / x ]_ B " _V )
14		dfrn4	|- ran B = ( B " _V )
15	14	csbeq2i	|- [_ A / x ]_ ran B = [_ A / x ]_ ( B " _V )
16		dfrn4	|- ran [_ A / x ]_ B = ( [_ A / x ]_ B " _V )
17	13 15 16	3eqtr4i	|- [_ A / x ]_ ran B = ran [_ A / x ]_ B