Theorem sbccow

Description: A composition law for class substitution. Version of sbcco with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 26-Sep-2003) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

	Ref	Expression
Assertion	sbccow	$$⊢\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		sbco2vv	$$⊢\left[z/y\right]\left[y/x\right]\phi \leftrightarrow \left[z/x\right]\phi$$
8		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$$
9	6 7 8	3bitr3ri	$$⊢\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \left[z/x\right]\phi$$
10		sbsbc	$$⊢\left[z/x\right]\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
11	9 10	bitri	$$⊢\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
12	3 4 11	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)$$
13	1 2 12	pm5.21nii	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$