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

Metamath Proof Explorer

Theorem dfima3

Description: Alternate definition of image. Compare definition (d) of Enderton p. 44. (Contributed by NM, 14-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	dfima3	$⊢ A [B] = \{y \| \exists x (x \in B \land ⟨x, y⟩ \in A)\}$

Proof

Step	Hyp	Ref	Expression
1		dfima2	$⊢ A [B] = \{y \| \exists x \in B x A y\}$
2		df-br	$⊢ x A y \leftrightarrow ⟨x, y⟩ \in A$
3	2	rexbii	$⊢ \exists x \in B x A y \leftrightarrow \exists x \in B ⟨x, y⟩ \in A$
4		df-rex	$⊢ \exists x \in B ⟨x, y⟩ \in A \leftrightarrow \exists x (x \in B \land ⟨x, y⟩ \in A)$
5	3 4	bitri	$⊢ \exists x \in B x A y \leftrightarrow \exists x (x \in B \land ⟨x, y⟩ \in A)$
6	5	abbii	$⊢ \{y \| \exists x \in B x A y\} = \{y \| \exists x (x \in B \land ⟨x, y⟩ \in A)\}$
7	1 6	eqtri	$⊢ A [B] = \{y \| \exists x (x \in B \land ⟨x, y⟩ \in A)\}$