Theorem csbfv12

Description: Move class substitution in and out of a function value. (Contributed by NM, 11-Nov-2005) (Revised by NM, 20-Aug-2018)

	Ref	Expression
Assertion	csbfv12	$$⊢⦋A/x⦌F\left(B\right)=⦋A/x⦌F\left(⦋A/x⦌B\right)$$

Proof

Step	Hyp	Ref	Expression
1		csbiota	$$⊢⦋A/x⦌\left(\iota y|BFy\right)=\left(\iota y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}BFy\right)$$
2		sbcbr123	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}BFy\leftrightarrow ⦋A/x⦌B⦋A/x⦌F⦋A/x⦌y$$
3		csbconstg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌y=y$$
4	3	breq2d	$$⊢A\in \mathrm{V}\to \left(⦋A/x⦌B⦋A/x⦌F⦋A/x⦌y\leftrightarrow ⦋A/x⦌B⦋A/x⦌Fy\right)$$
5	2 4	bitrid	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}BFy\leftrightarrow ⦋A/x⦌B⦋A/x⦌Fy\right)$$
6	5	iotabidv	$$⊢A\in \mathrm{V}\to \left(\iota y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}BFy\right)=\left(\iota y|⦋A/x⦌B⦋A/x⦌Fy\right)$$
7	1 6	eqtrid	$$⊢A\in \mathrm{V}\to ⦋A/x⦌\left(\iota y|BFy\right)=\left(\iota y|⦋A/x⦌B⦋A/x⦌Fy\right)$$
8		df-fv	$$⊢F\left(B\right)=\left(\iota y|BFy\right)$$
9	8	csbeq2i	$$⊢⦋A/x⦌F\left(B\right)=⦋A/x⦌\left(\iota y|BFy\right)$$
10		df-fv	$$⊢⦋A/x⦌F\left(⦋A/x⦌B\right)=\left(\iota y|⦋A/x⦌B⦋A/x⦌Fy\right)$$
11	7 9 10	3eqtr4g	$$⊢A\in \mathrm{V}\to ⦋A/x⦌F\left(B\right)=⦋A/x⦌F\left(⦋A/x⦌B\right)$$
12		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F\left(B\right)=\varnothing$$
13		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F=\varnothing$$
14	13	fveq1d	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F\left(⦋A/x⦌B\right)=\varnothing \left(⦋A/x⦌B\right)$$
15		0fv	$$⊢\varnothing \left(⦋A/x⦌B\right)=\varnothing$$
16	14 15	eqtr2di	$$⊢\neg A\in \mathrm{V}\to \varnothing =⦋A/x⦌F\left(⦋A/x⦌B\right)$$
17	12 16	eqtrd	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F\left(B\right)=⦋A/x⦌F\left(⦋A/x⦌B\right)$$
18	11 17	pm2.61i	$$⊢⦋A/x⦌F\left(B\right)=⦋A/x⦌F\left(⦋A/x⦌B\right)$$