This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elunirab

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

Ref Expression
Assertion elunirab ( 𝐴 ∈ ∪ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 eluniab ⊢ ( 𝐴 ∈ ∪ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
2 df-rab ⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
3 2 unieqi ⊢ ∪ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = ∪ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
4 3 eleq2i ⊢ ( 𝐴 ∈ ∪ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ 𝐴 ∈ ∪ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } )
5 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) ) )
6 an12 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ( 𝐴 ∈ 𝑥 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
7 6 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
8 5 7 bitri ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
9 1 4 8 3bitr4i ⊢ ( 𝐴 ∈ ∪ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) )