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 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑥𝐴 𝜑 }