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⦌\mathrm{ran}B=\mathrm{ran}⦋A/x⦌B$$

Proof

Step	Hyp	Ref	Expression
1		csbima12	$$⊢⦋A/x⦌B\left[\mathrm{V}\right]=⦋A/x⦌B\left[⦋A/x⦌\mathrm{V}\right]$$
2		csbconstg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌\mathrm{V}=\mathrm{V}$$
3	2	imaeq2d	$$⊢A\in \mathrm{V}\to ⦋A/x⦌B\left[⦋A/x⦌\mathrm{V}\right]=⦋A/x⦌B\left[\mathrm{V}\right]$$
4		0ima	$$⊢\varnothing \left[\mathrm{V}\right]=\varnothing$$
5	4	eqcomi	$$⊢\varnothing =\varnothing \left[\mathrm{V}\right]$$
6		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B=\varnothing$$
7	6	imaeq1d	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B\left[⦋A/x⦌\mathrm{V}\right]=\varnothing \left[⦋A/x⦌\mathrm{V}\right]$$
8		0ima	$$⊢\varnothing \left[⦋A/x⦌\mathrm{V}\right]=\varnothing$$
9	7 8	syl6eq	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B\left[⦋A/x⦌\mathrm{V}\right]=\varnothing$$
10	6	imaeq1d	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B\left[\mathrm{V}\right]=\varnothing \left[\mathrm{V}\right]$$
11	5 9 10	3eqtr4a	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B\left[⦋A/x⦌\mathrm{V}\right]=⦋A/x⦌B\left[\mathrm{V}\right]$$
12	3 11	pm2.61i	$$⊢⦋A/x⦌B\left[⦋A/x⦌\mathrm{V}\right]=⦋A/x⦌B\left[\mathrm{V}\right]$$
13	1 12	eqtri	$$⊢⦋A/x⦌B\left[\mathrm{V}\right]=⦋A/x⦌B\left[\mathrm{V}\right]$$
14		dfrn4	$$⊢\mathrm{ran}B=B\left[\mathrm{V}\right]$$
15	14	csbeq2i	$$⊢⦋A/x⦌\mathrm{ran}B=⦋A/x⦌B\left[\mathrm{V}\right]$$
16		dfrn4	$$⊢\mathrm{ran}⦋A/x⦌B=⦋A/x⦌B\left[\mathrm{V}\right]$$
17	13 15 16	3eqtr4i	$$⊢⦋A/x⦌\mathrm{ran}B=\mathrm{ran}⦋A/x⦌B$$