# Metamath Proof Explorer

## Theorem eliun

Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003)

Ref Expression
Assertion eliun ${⊢}{A}\in \bigcup _{{x}\in {B}}{C}↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{A}\in {C}$

### Proof

Step Hyp Ref Expression
1 elex ${⊢}{A}\in \bigcup _{{x}\in {B}}{C}\to {A}\in \mathrm{V}$
2 elex ${⊢}{A}\in {C}\to {A}\in \mathrm{V}$
3 2 rexlimivw ${⊢}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{A}\in {C}\to {A}\in \mathrm{V}$
4 eleq1 ${⊢}{y}={A}\to \left({y}\in {C}↔{A}\in {C}\right)$
5 4 rexbidv ${⊢}{y}={A}\to \left(\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{y}\in {C}↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{A}\in {C}\right)$
6 df-iun ${⊢}\bigcup _{{x}\in {B}}{C}=\left\{{y}|\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{y}\in {C}\right\}$
7 5 6 elab2g ${⊢}{A}\in \mathrm{V}\to \left({A}\in \bigcup _{{x}\in {B}}{C}↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{A}\in {C}\right)$
8 1 3 7 pm5.21nii ${⊢}{A}\in \bigcup _{{x}\in {B}}{C}↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{A}\in {C}$