Theorem csbab

Description: Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005) (Revised by NM, 19-Aug-2018)

	Ref	Expression
Assertion	csbab	$$⊢⦋A/x⦌\left\{y|\phi \right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-clab	$$⊢z\in \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}\leftrightarrow \left[z/y\right]\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
2		sbsbc	$$⊢\left[z/y\right]\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
3	1 2	bitri	$$⊢z\in \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}\leftrightarrow \underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
4		sbccom	$$⊢\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
5		df-clab	$$⊢z\in \left\{y|\phi \right\}\leftrightarrow \left[z/y\right]\phi$$
6		sbsbc	$$⊢\left[z/y\right]\phi \leftrightarrow \underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
7	5 6	bitri	$$⊢z\in \left\{y|\phi \right\}\leftrightarrow \underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
8	7	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in \left\{y|\phi \right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
9	4 8	bitr4i	$$⊢\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in \left\{y|\phi \right\}$$
10		sbcel2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in \left\{y|\phi \right\}\leftrightarrow z\in ⦋A/x⦌\left\{y|\phi \right\}$$
11	3 9 10	3bitrri	$$⊢z\in ⦋A/x⦌\left\{y|\phi \right\}\leftrightarrow z\in \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}$$
12	11	eqriv	$$⊢⦋A/x⦌\left\{y|\phi \right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right\}$$