Theorem csbnestgf

Description: Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker csbnestgfw when possible. (Contributed by NM, 23-Nov-2005) (Proof shortened by Mario Carneiro, 10-Nov-2016) (New usage is discouraged.)

	Ref	Expression
Assertion	csbnestgf	$$⊢\left(A\in V\wedge \forall y\underset{\_}{Ⅎ}xC\right)\to ⦋A/x⦌⦋B/y⦌C=⦋⦋A/x⦌B/y⦌C$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in V\to A\in \mathrm{V}$$
2		df-csb	$$⊢⦋B/y⦌C=\left\{z|\underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in C\right\}$$
3	2	abeq2i	$$⊢z\in ⦋B/y⦌C\leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in C$$
4	3	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in ⦋B/y⦌C\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in C$$
5		nfcr	$$⊢\underset{\_}{Ⅎ}xC\to Ⅎxz\in C$$
6	5	alimi	$$⊢\forall y\underset{\_}{Ⅎ}xC\to \forall yℲxz\in C$$
7		sbcnestgf	$$⊢\left(A\in \mathrm{V}\wedge \forall yℲxz\in C\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in C\leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}z\in C\right)$$
8	6 7	sylan2	$$⊢\left(A\in \mathrm{V}\wedge \forall y\underset{\_}{Ⅎ}xC\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in C\leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}z\in C\right)$$
9	4 8	bitrid	$$⊢\left(A\in \mathrm{V}\wedge \forall y\underset{\_}{Ⅎ}xC\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in ⦋B/y⦌C\leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}z\in C\right)$$
10	9	abbidv	$$⊢\left(A\in \mathrm{V}\wedge \forall y\underset{\_}{Ⅎ}xC\right)\to \left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in ⦋B/y⦌C\right\}=\left\{z|\underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}z\in C\right\}$$
11	1 10	sylan	$$⊢\left(A\in V\wedge \forall y\underset{\_}{Ⅎ}xC\right)\to \left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in ⦋B/y⦌C\right\}=\left\{z|\underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}z\in C\right\}$$
12		df-csb	$$⊢⦋A/x⦌⦋B/y⦌C=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in ⦋B/y⦌C\right\}$$
13		df-csb	$$⊢⦋⦋A/x⦌B/y⦌C=\left\{z|\underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}z\in C\right\}$$
14	11 12 13	3eqtr4g	$$⊢\left(A\in V\wedge \forall y\underset{\_}{Ⅎ}xC\right)\to ⦋A/x⦌⦋B/y⦌C=⦋⦋A/x⦌B/y⦌C$$