Theorem sbcco3g

Description: Composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sbcco3gw when possible. (Contributed by NM, 27-Nov-2005) (Revised by Mario Carneiro, 11-Nov-2016) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sbcco3g.1	$$⊢x=A\to B=C$$
Assertion	sbcco3g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/y\underset{\dot{}}{]}\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcco3g.1	$$⊢x=A\to B=C$$
2		sbcnestg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\phi \right)$$
3		elex	$$⊢A\in V\to A\in \mathrm{V}$$
4		nfcvd	$$⊢A\in \mathrm{V}\to \underset{\_}{Ⅎ}xC$$
5	4 1	csbiegf	$$⊢A\in \mathrm{V}\to ⦋A/x⦌B=C$$
6		dfsbcq	$$⊢⦋A/x⦌B=C\to \left(\underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/y\underset{\dot{}}{]}\phi \right)$$
7	3 5 6	3syl	$$⊢A\in V\to \left(\underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/y\underset{\dot{}}{]}\phi \right)$$
8	2 7	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/y\underset{\dot{}}{]}\phi \right)$$