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∈BA∈x∧φ

Proof

Step Hyp Ref Expression
1 eluniab ⊢A∈⋃x|x∈B∧φ↔∃xA∈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∈BA∈x∧φ↔∃xx∈B∧A∈x∧φ
6 an12 ⊢x∈B∧A∈x∧φ↔A∈x∧x∈B∧φ
7 6 exbii ⊢∃xx∈B∧A∈x∧φ↔∃xA∈x∧x∈B∧φ
8 5 7 bitri ⊢∃x∈BA∈x∧φ↔∃xA∈x∧x∈B∧φ
9 1 4 8 3bitr4i ⊢A∈⋃x∈B|φ↔∃x∈BA∈x∧φ