# Metamath Proof Explorer

## Theorem nfunid

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

Ref Expression
Hypothesis nfunid.3 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
Assertion nfunid ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\bigcup {A}$

### Proof

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