Theorem nfunidALT2

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

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

Proof

Step	Hyp	Ref	Expression
1		nfunidALT2.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
2		nfaba1	$$⊢\underset{\_}{Ⅎ}x\left\{y|\forall xy\in A\right\}$$
3	2	nfuni	$$⊢\underset{\_}{Ⅎ}x\bigcup \left\{y|\forall xy\in A\right\}$$
4		nfnfc1	$$⊢Ⅎx\underset{\_}{Ⅎ}xA$$
5		abidnf	$$⊢\underset{\_}{Ⅎ}xA\to \left\{y|\forall xy\in A\right\}=A$$
6	5	unieqd	$$⊢\underset{\_}{Ⅎ}xA\to \bigcup \left\{y|\forall xy\in A\right\}=\bigcup A$$
7	4 6	nfceqdf	$$⊢\underset{\_}{Ⅎ}xA\to \left(\underset{\_}{Ⅎ}x\bigcup \left\{y|\forall xy\in A\right\}\leftrightarrow \underset{\_}{Ⅎ}x\bigcup A\right)$$
8	1 7	syl	$$⊢\phi \to \left(\underset{\_}{Ⅎ}x\bigcup \left\{y|\forall xy\in A\right\}\leftrightarrow \underset{\_}{Ⅎ}x\bigcup A\right)$$
9	3 8	mpbii	$$⊢\phi \to \underset{\_}{Ⅎ}x\bigcup A$$