Metamath Proof Explorer

Theorem eluni

Description: Membership in class union. (Contributed by NM, 22-May-1994)

Ref Expression
Assertion eluni ⊢ A ∈ ⋃ B ↔ ∃ x A ∈ x ∧ x ∈ B

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ ⋃ B → A ∈ V
2 elex ⊢ A ∈ x → A ∈ V
3 2 adantr ⊢ A ∈ x ∧ x ∈ B → A ∈ V
4 3 exlimiv ⊢ ∃ x A ∈ x ∧ x ∈ B → A ∈ V
5 eleq1 ⊢ y = A → y ∈ x ↔ A ∈ x
6 5 anbi1d ⊢ y = A → y ∈ x ∧ x ∈ B ↔ A ∈ x ∧ x ∈ B
7 6 exbidv ⊢ y = A → ∃ x y ∈ x ∧ x ∈ B ↔ ∃ x A ∈ x ∧ x ∈ B
8 df-uni ⊢ ⋃ B = y | ∃ x y ∈ x ∧ x ∈ B
9 7 8 elab2g ⊢ A ∈ V → A ∈ ⋃ B ↔ ∃ x A ∈ x ∧ x ∈ B
10 1 4 9 pm5.21nii ⊢ A ∈ ⋃ B ↔ ∃ x A ∈ x ∧ x ∈ B