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 = y → x ∈ B ↔ y ∈ B
6 eleq1 ⊢ x = y → x ∈ C ↔ y ∈ C
7 5 6 orbi12d ⊢ x = y → x ∈ B ∨ x ∈ C ↔ y ∈ B ∨ y ∈ C
8 eleq1 ⊢ y = A → y ∈ B ↔ A ∈ B
9 eleq1 ⊢ y = A → y ∈ C ↔ A ∈ C
10 8 9 orbi12d ⊢ y = A → y ∈ B ∨ y ∈ C ↔ A ∈ B ∨ A ∈ C
11 df-un ⊢ B ∪ C = x | x ∈ B ∨ x ∈ C
12 7 10 11 elab2gw ⊢ A ∈ V → A ∈ B ∪ C ↔ A ∈ B ∨ A ∈ C
13 1 4 12 pm5.21nii ⊢ A ∈ B ∪ C ↔ A ∈ B ∨ A ∈ C