# Metamath Proof Explorer

## Theorem dmun

Description: The domain of a union is the union of domains. Exercise 56(a) of Enderton p. 65. (Contributed by NM, 12-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion dmun ${⊢}\mathrm{dom}\left({A}\cup {B}\right)=\mathrm{dom}{A}\cup \mathrm{dom}{B}$

### Proof

Step Hyp Ref Expression
1 unab ${⊢}\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{y}{A}{x}\right\}\cup \left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{y}{B}{x}\right\}=\left\{{y}|\left(\exists {x}\phantom{\rule{.4em}{0ex}}{y}{A}{x}\vee \exists {x}\phantom{\rule{.4em}{0ex}}{y}{B}{x}\right)\right\}$
2 brun ${⊢}{y}\left({A}\cup {B}\right){x}↔\left({y}{A}{x}\vee {y}{B}{x}\right)$
3 2 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{y}\left({A}\cup {B}\right){x}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{A}{x}\vee {y}{B}{x}\right)$
4 19.43 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}{A}{x}\vee {y}{B}{x}\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{y}{A}{x}\vee \exists {x}\phantom{\rule{.4em}{0ex}}{y}{B}{x}\right)$
5 3 4 bitr2i ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{y}{A}{x}\vee \exists {x}\phantom{\rule{.4em}{0ex}}{y}{B}{x}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}{y}\left({A}\cup {B}\right){x}$
6 5 abbii ${⊢}\left\{{y}|\left(\exists {x}\phantom{\rule{.4em}{0ex}}{y}{A}{x}\vee \exists {x}\phantom{\rule{.4em}{0ex}}{y}{B}{x}\right)\right\}=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{y}\left({A}\cup {B}\right){x}\right\}$
7 1 6 eqtri ${⊢}\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{y}{A}{x}\right\}\cup \left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{y}{B}{x}\right\}=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{y}\left({A}\cup {B}\right){x}\right\}$
8 df-dm ${⊢}\mathrm{dom}{A}=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{y}{A}{x}\right\}$
9 df-dm ${⊢}\mathrm{dom}{B}=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{y}{B}{x}\right\}$
10 8 9 uneq12i ${⊢}\mathrm{dom}{A}\cup \mathrm{dom}{B}=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{y}{A}{x}\right\}\cup \left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{y}{B}{x}\right\}$
11 df-dm ${⊢}\mathrm{dom}\left({A}\cup {B}\right)=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}{y}\left({A}\cup {B}\right){x}\right\}$
12 7 10 11 3eqtr4ri ${⊢}\mathrm{dom}\left({A}\cup {B}\right)=\mathrm{dom}{A}\cup \mathrm{dom}{B}$