Theorem csbima12

Description: Move class substitution in and out of the image of a function. (Contributed by FL, 15-Dec-2006) (Revised by NM, 20-Aug-2018)

	Ref	Expression
Assertion	csbima12	$$⊢⦋A/x⦌F\left[B\right]=⦋A/x⦌F\left[⦋A/x⦌B\right]$$

Proof

Step	Hyp	Ref	Expression
1		csbeq1	$$⊢y=A\to ⦋y/x⦌F\left[B\right]=⦋A/x⦌F\left[B\right]$$
2		csbeq1	$$⊢y=A\to ⦋y/x⦌F=⦋A/x⦌F$$
3		csbeq1	$$⊢y=A\to ⦋y/x⦌B=⦋A/x⦌B$$
4	2 3	imaeq12d	$$⊢y=A\to ⦋y/x⦌F\left[⦋y/x⦌B\right]=⦋A/x⦌F\left[⦋A/x⦌B\right]$$
5	1 4	eqeq12d	$$⊢y=A\to \left(⦋y/x⦌F\left[B\right]=⦋y/x⦌F\left[⦋y/x⦌B\right]\leftrightarrow ⦋A/x⦌F\left[B\right]=⦋A/x⦌F\left[⦋A/x⦌B\right]\right)$$
6		vex	$$⊢y\in \mathrm{V}$$
7		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌F$$
8		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
9	7 8	nfima	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌F\left[⦋y/x⦌B\right]$$
10		csbeq1a	$$⊢x=y\to F=⦋y/x⦌F$$
11		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
12	10 11	imaeq12d	$$⊢x=y\to F\left[B\right]=⦋y/x⦌F\left[⦋y/x⦌B\right]$$
13	6 9 12	csbief	$$⊢⦋y/x⦌F\left[B\right]=⦋y/x⦌F\left[⦋y/x⦌B\right]$$
14	5 13	vtoclg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌F\left[B\right]=⦋A/x⦌F\left[⦋A/x⦌B\right]$$
15		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F\left[B\right]=\varnothing$$
16		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B=\varnothing$$
17	16	imaeq2d	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F\left[⦋A/x⦌B\right]=⦋A/x⦌F\left[\varnothing \right]$$
18		ima0	$$⊢⦋A/x⦌F\left[\varnothing \right]=\varnothing$$
19	17 18	eqtr2di	$$⊢\neg A\in \mathrm{V}\to \varnothing =⦋A/x⦌F\left[⦋A/x⦌B\right]$$
20	15 19	eqtrd	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F\left[B\right]=⦋A/x⦌F\left[⦋A/x⦌B\right]$$
21	14 20	pm2.61i	$$⊢⦋A/x⦌F\left[B\right]=⦋A/x⦌F\left[⦋A/x⦌B\right]$$