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

Metamath Proof Explorer

Theorem dfima2

Description: Alternate definition of image. Compare definition (d) of Enderton p. 44. (Contributed by NM, 19-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by Peter Mazsa, 2-Oct-2022)

		Ref	Expression
	Assertion	dfima2	$⊢ A [B] = \{y \| \exists x \in B x A y\}$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$⊢ A [B] = ran ({A ↾}_{B})$
2		dfrn2	$⊢ ran ({A ↾}_{B}) = \{y \| \exists x x ({A ↾}_{B}) y\}$
3		brres	$⊢ y \in V \to (x ({A ↾}_{B}) y \leftrightarrow (x \in B \land x A y))$
4	3	elv	$⊢ x ({A ↾}_{B}) y \leftrightarrow (x \in B \land x A y)$
5	4	exbii	$⊢ \exists x x ({A ↾}_{B}) y \leftrightarrow \exists x (x \in B \land x A y)$
6		df-rex	$⊢ \exists x \in B x A y \leftrightarrow \exists x (x \in B \land x A y)$
7	5 6	bitr4i	$⊢ \exists x x ({A ↾}_{B}) y \leftrightarrow \exists x \in B x A y$
8	7	abbii	$⊢ \{y \| \exists x x ({A ↾}_{B}) y\} = \{y \| \exists x \in B x A y\}$
9	1 2 8	3eqtri	$⊢ A [B] = \{y \| \exists x \in B x A y\}$