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∈B∪C↔A∈B∨A∈C

Proof

Step Hyp Ref Expression
1 elex ⊢A∈B∪C→A∈V
2 elex ⊢A∈B→A∈V
3 elex ⊢A∈C→A∈V
4 2 3 jaoi ⊢A∈B∨A∈C→A∈V
5 eleq1 ⊢x=A→x∈B↔A∈B
6 eleq1 ⊢x=A→x∈C↔A∈C
7 5 6 orbi12d ⊢x=A→x∈B∨x∈C↔A∈B∨A∈C
8 df-un ⊢B∪C=x|x∈B∨x∈C
9 7 8 elab2g ⊢A∈V→A∈B∪C↔A∈B∨A∈C
10 1 4 9 pm5.21nii ⊢A∈B∪C↔A∈B∨A∈C