Theorem nfsbcd

Description: Deduction version of nfsbc . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfsbcdw when possible. (Contributed by NM, 23-Nov-2005) (Revised by Mario Carneiro, 12-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfsbcd.1	$$⊢Ⅎy\phi$$
	nfsbcd.2	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
	nfsbcd.3	$$⊢\phi \to Ⅎx\psi$$
Assertion	nfsbcd	$$⊢\phi \to Ⅎx\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\psi$$

Proof

Step	Hyp	Ref	Expression
1		nfsbcd.1	$$⊢Ⅎy\phi$$
2		nfsbcd.2	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
3		nfsbcd.3	$$⊢\phi \to Ⅎx\psi$$
4		df-sbc	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\psi \leftrightarrow A\in \left\{y|\psi \right\}$$
5	1 3	nfabd	$$⊢\phi \to \underset{\_}{Ⅎ}x\left\{y|\psi \right\}$$
6	2 5	nfeld	$$⊢\phi \to ℲxA\in \left\{y|\psi \right\}$$
7	4 6	nfxfrd	$$⊢\phi \to Ⅎx\underset{\dot{}}{[}A/y\underset{\dot{}}{]}\psi$$