Metamath Proof Explorer

Theorem eluni2

Description: Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999)

Ref Expression
Assertion eluni2 ⊢ A ∈ ⋃ B ↔ ∃ x ∈ B A ∈ x

Proof

Step Hyp Ref Expression
1 exancom ⊢ ∃ x A ∈ x ∧ x ∈ B ↔ ∃ x x ∈ B ∧ A ∈ x
2 eluni ⊢ A ∈ ⋃ B ↔ ∃ x A ∈ x ∧ x ∈ B
3 df-rex ⊢ ∃ x ∈ B A ∈ x ↔ ∃ x x ∈ B ∧ A ∈ x
4 1 2 3 3bitr4i ⊢ A ∈ ⋃ B ↔ ∃ x ∈ B A ∈ x