Theorem sbccsb

Description: Substitution into a wff expressed in terms of substitution into a class. (Contributed by NM, 15-Aug-2007) (Revised by NM, 18-Aug-2018)

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

Proof

Step	Hyp	Ref	Expression
1		abid	$$⊢y\in \left\{y|\phi \right\}\leftrightarrow \phi$$
2	1	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in \left\{y|\phi \right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
3		sbcel2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in \left\{y|\phi \right\}\leftrightarrow y\in ⦋A/x⦌\left\{y|\phi \right\}$$
4	2 3	bitr3i	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow y\in ⦋A/x⦌\left\{y|\phi \right\}$$