# Metamath Proof Explorer

## Theorem iunexg

Description: The existence of an indexed union. x is normally a free-variable parameter in B . (Contributed by NM, 23-Mar-2006)

Ref Expression
Assertion iunexg ${⊢}\left({A}\in {V}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {W}\right)\to \bigcup _{{x}\in {A}}{B}\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 dfiun2g ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {W}\to \bigcup _{{x}\in {A}}{B}=\bigcup \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}$
2 1 adantl ${⊢}\left({A}\in {V}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {W}\right)\to \bigcup _{{x}\in {A}}{B}=\bigcup \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}$
3 abrexexg ${⊢}{A}\in {V}\to \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}\in \mathrm{V}$
4 3 uniexd ${⊢}{A}\in {V}\to \bigcup \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}\in \mathrm{V}$
5 4 adantr ${⊢}\left({A}\in {V}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {W}\right)\to \bigcup \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}\in \mathrm{V}$
6 2 5 eqeltrd ${⊢}\left({A}\in {V}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {W}\right)\to \bigcup _{{x}\in {A}}{B}\in \mathrm{V}$