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 elequ1 ⊢ y = z → y ∈ x ↔ z ∈ x
6 5 anbi1d ⊢ y = z → y ∈ x ∧ x ∈ B ↔ z ∈ x ∧ x ∈ B
7 6 exbidv ⊢ y = z → ∃ x y ∈ x ∧ x ∈ B ↔ ∃ x z ∈ x ∧ x ∈ B
8 eleq1 ⊢ z = A → z ∈ x ↔ A ∈ x
9 8 anbi1d ⊢ z = A → z ∈ x ∧ x ∈ B ↔ A ∈ x ∧ x ∈ B
10 9 exbidv ⊢ z = A → ∃ x z ∈ x ∧ x ∈ B ↔ ∃ x A ∈ x ∧ x ∈ B
11 df-uni ⊢ ⋃ B = y | ∃ x y ∈ x ∧ x ∈ B
12 7 10 11 elab2gw ⊢ A ∈ V → A ∈ ⋃ B ↔ ∃ x A ∈ x ∧ x ∈ B
13 1 4 12 pm5.21nii ⊢ A ∈ ⋃ B ↔ ∃ x A ∈ x ∧ x ∈ B