Theorem csbafv212g

Description: Move class substitution in and out of a function value, analogous to csbfv12 , with a direct proof proposed by Mario Carneiro, analogous to csbov123 . (Contributed by AV, 4-Sep-2022)

	Ref	Expression
Assertion	csbafv212g	$$⊢A\in V\to ⦋A/x⦌\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}B\right)=\left(⦋A/x⦌F\mathrm{\text{'}\text{'}\text{'}\text{'}}⦋A/x⦌B\right)$$

Proof

Step	Hyp	Ref	Expression
1		csbeq1	$$⊢y=A\to ⦋y/x⦌\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}B\right)=⦋A/x⦌\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}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	afv2eq12d	$$⊢y=A\to \left(⦋y/x⦌F\mathrm{\text{'}\text{'}\text{'}\text{'}}⦋y/x⦌B\right)=\left(⦋A/x⦌F\mathrm{\text{'}\text{'}\text{'}\text{'}}⦋A/x⦌B\right)$$
5	1 4	eqeq12d	$$⊢y=A\to \left(⦋y/x⦌\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}B\right)=\left(⦋y/x⦌F\mathrm{\text{'}\text{'}\text{'}\text{'}}⦋y/x⦌B\right)\leftrightarrow ⦋A/x⦌\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}B\right)=\left(⦋A/x⦌F\mathrm{\text{'}\text{'}\text{'}\text{'}}⦋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	nfafv2	$$⊢\underset{\_}{Ⅎ}x\left(⦋y/x⦌F\mathrm{\text{'}\text{'}\text{'}\text{'}}⦋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	afv2eq12d	$$⊢x=y\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}B\right)=\left(⦋y/x⦌F\mathrm{\text{'}\text{'}\text{'}\text{'}}⦋y/x⦌B\right)$$
13	6 9 12	csbief	$$⊢⦋y/x⦌\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}B\right)=\left(⦋y/x⦌F\mathrm{\text{'}\text{'}\text{'}\text{'}}⦋y/x⦌B\right)$$
14	5 13	vtoclg	$$⊢A\in V\to ⦋A/x⦌\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}B\right)=\left(⦋A/x⦌F\mathrm{\text{'}\text{'}\text{'}\text{'}}⦋A/x⦌B\right)$$