Theorem dfsbcq2

Description: This theorem, which is similar to Theorem 6.7 of Quine p. 42 and holds under both our definition and Quine's, relates logic substitution df-sb and substitution for class variables df-sbc . Unlike Quine, we use a different syntax for each in order to avoid overloading it. See remarks in dfsbcq . (Contributed by NM, 31-Dec-2016)

	Ref	Expression
Assertion	dfsbcq2	$$⊢y=A\to \left(\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢y=A\to \left(y\in \left\{x|\phi \right\}\leftrightarrow A\in \left\{x|\phi \right\}\right)$$
2		df-clab	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \left[y/x\right]\phi$$
3		df-sbc	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow A\in \left\{x|\phi \right\}$$
4	3	bicomi	$$⊢A\in \left\{x|\phi \right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
5	1 2 4	3bitr3g	$$⊢y=A\to \left(\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$