Theorem csbco

Description: Composition law for chained substitutions into a class. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker csbcow when possible. (Contributed by NM, 10-Nov-2005) (New usage is discouraged.)

	Ref	Expression
Assertion	csbco	$$⊢⦋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		sbcco	$$⊢\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$$