# Metamath Proof Explorer

## Theorem elun

Description: Expansion of membership in class union. Theorem 12 of Suppes p. 25. (Contributed by NM, 7-Aug-1994)

Ref Expression
Assertion elun ${⊢}{A}\in \left({B}\cup {C}\right)↔\left({A}\in {B}\vee {A}\in {C}\right)$

### Proof

Step Hyp Ref Expression
1 elex ${⊢}{A}\in \left({B}\cup {C}\right)\to {A}\in \mathrm{V}$
2 elex ${⊢}{A}\in {B}\to {A}\in \mathrm{V}$
3 elex ${⊢}{A}\in {C}\to {A}\in \mathrm{V}$
4 2 3 jaoi ${⊢}\left({A}\in {B}\vee {A}\in {C}\right)\to {A}\in \mathrm{V}$
5 eleq1 ${⊢}{x}={A}\to \left({x}\in {B}↔{A}\in {B}\right)$
6 eleq1 ${⊢}{x}={A}\to \left({x}\in {C}↔{A}\in {C}\right)$
7 5 6 orbi12d ${⊢}{x}={A}\to \left(\left({x}\in {B}\vee {x}\in {C}\right)↔\left({A}\in {B}\vee {A}\in {C}\right)\right)$
8 df-un ${⊢}{B}\cup {C}=\left\{{x}|\left({x}\in {B}\vee {x}\in {C}\right)\right\}$
9 7 8 elab2g ${⊢}{A}\in \mathrm{V}\to \left({A}\in \left({B}\cup {C}\right)↔\left({A}\in {B}\vee {A}\in {C}\right)\right)$
10 1 4 9 pm5.21nii ${⊢}{A}\in \left({B}\cup {C}\right)↔\left({A}\in {B}\vee {A}\in {C}\right)$