Theorem sbccsb2

Description: Substitution into a wff expressed in using substitution into a class. (Contributed by NM, 27-Nov-2005) (Revised by NM, 18-Aug-2018)

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

Proof

Step	Hyp	Ref	Expression
1		sbcex	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to A\in \mathrm{V}$$
2		elex	$$⊢A\in ⦋A/x⦌\left\{x|\phi \right\}\to A\in \mathrm{V}$$
3		abid	$$⊢x\in \left\{x|\phi \right\}\leftrightarrow \phi$$
4	3	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x\in \left\{x|\phi \right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
5		sbcel12	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x\in \left\{x|\phi \right\}\leftrightarrow ⦋A/x⦌x\in ⦋A/x⦌\left\{x|\phi \right\}$$
6		csbvarg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌x=A$$
7	6	eleq1d	$$⊢A\in \mathrm{V}\to \left(⦋A/x⦌x\in ⦋A/x⦌\left\{x|\phi \right\}\leftrightarrow A\in ⦋A/x⦌\left\{x|\phi \right\}\right)$$
8	5 7	bitrid	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x\in \left\{x|\phi \right\}\leftrightarrow A\in ⦋A/x⦌\left\{x|\phi \right\}\right)$$
9	4 8	bitr3id	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow A\in ⦋A/x⦌\left\{x|\phi \right\}\right)$$
10	1 2 9	pm5.21nii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow A\in ⦋A/x⦌\left\{x|\phi \right\}$$