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

Metamath Proof Explorer

Theorem imaopab

Description: The image of a class of ordered pairs. (Contributed by Steven Nguyen, 6-Jun-2023)

Ref Expression
Assertion imaopab ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 }

Proof

Step Hyp Ref Expression
1 df-ima ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } “ 𝐴 ) = ran ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↾ 𝐴 )
2 resopab ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
3 2 rneqi ⊢ ran ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↾ 𝐴 ) = ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
4 rnopab ⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
5 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
6 5 abbii ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
7 4 6 eqtr4i ⊢ ran { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 }
8 1 3 7 3eqtri ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 }