Metamath Proof Explorer

Theorem elunirab

Description: Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006)

Ref Expression
Assertion elunirab ⊢ A ∈ ⋃ x ∈ B | φ ↔ ∃ x ∈ B A ∈ x ∧ φ

Proof

Step Hyp Ref Expression
1 eluniab ⊢ A ∈ ⋃ x | x ∈ B ∧ φ ↔ ∃ x A ∈ x ∧ x ∈ B ∧ φ
2 df-rab ⊢ x ∈ B | φ = x | x ∈ B ∧ φ
3 2 unieqi ⊢ ⋃ x ∈ B | φ = ⋃ x | x ∈ B ∧ φ
4 3 eleq2i ⊢ A ∈ ⋃ x ∈ B | φ ↔ A ∈ ⋃ x | x ∈ B ∧ φ
5 df-rex ⊢ ∃ x ∈ B A ∈ x ∧ φ ↔ ∃ x x ∈ B ∧ A ∈ x ∧ φ
6 an12 ⊢ x ∈ B ∧ A ∈ x ∧ φ ↔ A ∈ x ∧ x ∈ B ∧ φ
7 6 exbii ⊢ ∃ x x ∈ B ∧ A ∈ x ∧ φ ↔ ∃ x A ∈ x ∧ x ∈ B ∧ φ
8 5 7 bitri ⊢ ∃ x ∈ B A ∈ x ∧ φ ↔ ∃ x A ∈ x ∧ x ∈ B ∧ φ
9 1 4 8 3bitr4i ⊢ A ∈ ⋃ x ∈ B | φ ↔ ∃ x ∈ B A ∈ x ∧ φ