Theorem nfiotadw

Description: Deduction version of nfiotaw . Version of nfiotad with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 18-Feb-2013) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

	Ref	Expression
Hypotheses	nfiotadw.1	$$⊢Ⅎy\phi$$
	nfiotadw.2	$$⊢\phi \to Ⅎx\psi$$
Assertion	nfiotadw	$$⊢\phi \to \underset{\_}{Ⅎ}x\left(\iota y|\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfiotadw.1	$$⊢Ⅎy\phi$$
2		nfiotadw.2	$$⊢\phi \to Ⅎx\psi$$
3		dfiota2	$$⊢\left(\iota y|\psi \right)=\bigcup \left\{z|\forall y\left(\psi \leftrightarrow y=z\right)\right\}$$
4		nfv	$$⊢Ⅎz\phi$$
5		nfvd	$$⊢\phi \to Ⅎxy=z$$
6	2 5	nfbid	$$⊢\phi \to Ⅎx\left(\psi \leftrightarrow y=z\right)$$
7	1 6	nfald	$$⊢\phi \to Ⅎx\forall y\left(\psi \leftrightarrow y=z\right)$$
8	4 7	nfabdw	$$⊢\phi \to \underset{\_}{Ⅎ}x\left\{z|\forall y\left(\psi \leftrightarrow y=z\right)\right\}$$
9	8	nfunid	$$⊢\phi \to \underset{\_}{Ⅎ}x\bigcup \left\{z|\forall y\left(\psi \leftrightarrow y=z\right)\right\}$$
10	3 9	nfcxfrd	$$⊢\phi \to \underset{\_}{Ⅎ}x\left(\iota y|\psi \right)$$