Theorem nfsbc1d

Description: Deduction version of nfsbc1 . (Contributed by NM, 23-May-2006) (Revised by Mario Carneiro, 12-Oct-2016)

	Ref	Expression
Hypothesis	nfsbc1d.2	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
Assertion	nfsbc1d	$$⊢\phi \to Ⅎx\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi$$

Proof

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