Theorem nfunidALT

Description: Deduction version of nfuni . (Contributed by NM, 19-Nov-2020) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nfunidALT.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
2		abidnf	$$⊢\underset{\_}{Ⅎ}xA\to \left\{y|\forall xy\in A\right\}=A$$
3	2	unieqd	$$⊢\underset{\_}{Ⅎ}xA\to \bigcup \left\{y|\forall xy\in A\right\}=\bigcup A$$
4		nfaba1	$$⊢\underset{\_}{Ⅎ}x\left\{y|\forall xy\in A\right\}$$
5	4	nfuni	$$⊢\underset{\_}{Ⅎ}x\bigcup \left\{y|\forall xy\in A\right\}$$
6	1 3 5	nfded	$$⊢\phi \to \underset{\_}{Ⅎ}x\bigcup A$$