Theorem sbc8g

Description: This is the closest we can get to df-sbc if we start from dfsbcq (see its comments) and dfsbcq2 . (Contributed by NM, 18-Nov-2008) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof modification is discouraged.)

	Ref	Expression
Assertion	sbc8g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow A\in \left\{x|\phi \right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfsbcq	$$⊢y=A\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
2		eleq1	$$⊢y=A\to \left(y\in \left\{x|\phi \right\}\leftrightarrow A\in \left\{x|\phi \right\}\right)$$
3		df-clab	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \left[y/x\right]\phi$$
4		equid	$$⊢y=y$$
5		dfsbcq2	$$⊢y=y\to \left(\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
6	4 5	ax-mp	$$⊢\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
7	3 6	bitr2i	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow y\in \left\{x|\phi \right\}$$
8	1 2 7	vtoclbg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow A\in \left\{x|\phi \right\}\right)$$