Theorem nfunid

Description: Deduction version of nfuni . (Contributed by NM, 18-Feb-2013)

	Ref	Expression
Hypothesis	nfunid.3	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
Assertion	nfunid	$$⊢\phi \to \underset{\_}{Ⅎ}x\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		nfunid.3	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
2		dfuni2	$$⊢\bigcup A=\left\{y|\exists z\in Ay\in z\right\}$$
3		nfv	$$⊢Ⅎy\phi$$
4		nfv	$$⊢Ⅎz\phi$$
5		nfvd	$$⊢\phi \to Ⅎxy\in z$$
6	4 1 5	nfrexdw	$$⊢\phi \to Ⅎx\exists z\in Ay\in z$$
7	3 6	nfabdw	$$⊢\phi \to \underset{\_}{Ⅎ}x\left\{y|\exists z\in Ay\in z\right\}$$
8	2 7	nfcxfrd	$$⊢\phi \to \underset{\_}{Ⅎ}x\bigcup A$$