Metamath Proof Explorer

Theorem elunii

Description: Membership in class union. (Contributed by NM, 24-Mar-1995)

Ref Expression
Assertion elunii ⊢ A ∈ B ∧ B ∈ C → A ∈ ⋃ C

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ x = B → A ∈ x ↔ A ∈ B
2 eleq1 ⊢ x = B → x ∈ C ↔ B ∈ C
3 1 2 anbi12d ⊢ x = B → A ∈ x ∧ x ∈ C ↔ A ∈ B ∧ B ∈ C
4 3 spcegv ⊢ B ∈ C → A ∈ B ∧ B ∈ C → ∃ x A ∈ x ∧ x ∈ C
5 4 anabsi7 ⊢ A ∈ B ∧ B ∈ C → ∃ x A ∈ x ∧ x ∈ C
6 eluni ⊢ A ∈ ⋃ C ↔ ∃ x A ∈ x ∧ x ∈ C
7 5 6 sylibr ⊢ A ∈ B ∧ B ∈ C → A ∈ ⋃ C