Theorem csbcow

Description: Composition law for chained substitutions into a class. Version of csbco with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 10-Nov-2005) (Revised by Gino Giotto, 10-Jan-2024)

	Ref	Expression
Assertion	csbcow	$$⊢⦋A/y⦌⦋y/x⦌B=⦋A/x⦌B$$

Proof

Step	Hyp	Ref	Expression
1		df-csb	$$⊢⦋y/x⦌B=\left\{z|\underset{\dot{}}{[}y/x\underset{\dot{}}{]}z\in B\right\}$$
2	1	abeq2i	$$⊢z\in ⦋y/x⦌B\leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}z\in B$$
3	2	sbcbii	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}z\in ⦋y/x⦌B\leftrightarrow \underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}z\in B$$
4		sbccow	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}z\in B\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in B$$
5	3 4	bitri	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}z\in ⦋y/x⦌B\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in B$$
6	5	abbii	$$⊢\left\{z|\underset{\dot{}}{[}A/y\underset{\dot{}}{]}z\in ⦋y/x⦌B\right\}=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in B\right\}$$
7		df-csb	$$⊢⦋A/y⦌⦋y/x⦌B=\left\{z|\underset{\dot{}}{[}A/y\underset{\dot{}}{]}z\in ⦋y/x⦌B\right\}$$
8		df-csb	$$⊢⦋A/x⦌B=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in B\right\}$$
9	6 7 8	3eqtr4i	$$⊢⦋A/y⦌⦋y/x⦌B=⦋A/x⦌B$$