# Metamath Proof Explorer

## Theorem eluni

Description: Membership in class union. (Contributed by NM, 22-May-1994)

Ref Expression
Assertion eluni ${⊢}{A}\in \bigcup {B}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}\wedge {x}\in {B}\right)$

### Proof

Step Hyp Ref Expression
1 elex ${⊢}{A}\in \bigcup {B}\to {A}\in \mathrm{V}$
2 elex ${⊢}{A}\in {x}\to {A}\in \mathrm{V}$
3 2 adantr ${⊢}\left({A}\in {x}\wedge {x}\in {B}\right)\to {A}\in \mathrm{V}$
4 3 exlimiv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}\wedge {x}\in {B}\right)\to {A}\in \mathrm{V}$
5 eleq1 ${⊢}{y}={A}\to \left({y}\in {x}↔{A}\in {x}\right)$
6 5 anbi1d ${⊢}{y}={A}\to \left(\left({y}\in {x}\wedge {x}\in {B}\right)↔\left({A}\in {x}\wedge {x}\in {B}\right)\right)$
7 6 exbidv ${⊢}{y}={A}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\wedge {x}\in {B}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}\wedge {x}\in {B}\right)\right)$
8 df-uni ${⊢}\bigcup {B}=\left\{{y}|\exists {x}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}\wedge {x}\in {B}\right)\right\}$
9 7 8 elab2g ${⊢}{A}\in \mathrm{V}\to \left({A}\in \bigcup {B}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}\wedge {x}\in {B}\right)\right)$
10 1 4 9 pm5.21nii ${⊢}{A}\in \bigcup {B}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({A}\in {x}\wedge {x}\in {B}\right)$