imaopab

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

		Ref	Expression
	Assertion	imaopab	$⊢ \{⟨x, y⟩ \| φ\} [A] = \{y \| \exists x \in A φ\}$

Step	Hyp	Ref	Expression
1		df-ima	$⊢ \{⟨x, y⟩ \| φ\} [A] = ran ({\{⟨x, y⟩ \| φ\} ↾}_{A})$
2		resopab	$⊢ {\{⟨x, y⟩ \| φ\} ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land φ)\}$
3	2	rneqi	$⊢ ran ({\{⟨x, y⟩ \| φ\} ↾}_{A}) = ran \{⟨x, y⟩ \| (x \in A \land φ)\}$
4		rnopab	$⊢ ran \{⟨x, y⟩ \| (x \in A \land φ)\} = \{y \| \exists x (x \in A \land φ)\}$
5		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
6	5	abbii	$⊢ \{y \| \exists x \in A φ\} = \{y \| \exists x (x \in A \land φ)\}$
7	4 6	eqtr4i	$⊢ ran \{⟨x, y⟩ \| (x \in A \land φ)\} = \{y \| \exists x \in A φ\}$
8	1 3 7	3eqtri	$⊢ \{⟨x, y⟩ \| φ\} [A] = \{y \| \exists x \in A φ\}$

Metamath Proof Explorer