Theorem sbcco

Description: A composition law for class substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sbccow when possible. (Contributed by NM, 26-Sep-2003) (Revised by Mario Carneiro, 13-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Assertion	sbcco	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbcex	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to A\in \mathrm{V}$$
2		sbcex	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to A\in \mathrm{V}$$
3		dfsbcq	$$⊢z=A\to \left(\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
4		dfsbcq	$$⊢z=A\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
5		sbsbc	$$⊢\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
6	5	sbbii	$$⊢\left[z/y\right]\left[y/x\right]\phi \leftrightarrow \left[z/y\right]\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
7		nfv	$$⊢Ⅎy\phi$$
8	7	sbco2	$$⊢\left[z/y\right]\left[y/x\right]\phi \leftrightarrow \left[z/x\right]\phi$$
9		sbsbc	$$⊢\left[z/y\right]\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
10	6 8 9	3bitr3ri	$$⊢\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \left[z/x\right]\phi$$
11		sbsbc	$$⊢\left[z/x\right]\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
12	10 11	bitri	$$⊢\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
13	3 4 12	vtoclbg	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
14	1 2 13	pm5.21nii	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$