# Metamath Proof Explorer

## Theorem nfun

Description: Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003) (Revised by Mario Carneiro, 14-Oct-2016)

Ref Expression
Hypotheses nfun.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
nfun.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
Assertion nfun ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({A}\cup {B}\right)$

### Proof

Step Hyp Ref Expression
1 nfun.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 nfun.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
3 df-un ${⊢}{A}\cup {B}=\left\{{y}|\left({y}\in {A}\vee {y}\in {B}\right)\right\}$
4 1 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$
5 2 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
6 4 5 nfor ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\vee {y}\in {B}\right)$
7 6 nfab ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{y}|\left({y}\in {A}\vee {y}\in {B}\right)\right\}$
8 3 7 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({A}\cup {B}\right)$