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