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\left[B\right]=\left\{y|\exists x\left(x\in B\wedge ⟨x,y⟩\in A\right)\right\}$$

Proof

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