Theorem nfsbcdw

Description: Deduction version of nfsbcw . Version of nfsbcd with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 23-Nov-2005) (Revised by Gino Giotto, 10-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		nfsbcdw.1	$$⊢Ⅎy\phi$$
2		nfsbcdw.2	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
3		nfsbcdw.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	nfabdw	$$⊢\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$$