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