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\left[B\right]=\left\{y|\exists x\in BxAy\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$$⊢A\left[B\right]=\mathrm{ran}\left({A\upharpoonright }_B\right)$$
2		dfrn2	$$⊢\mathrm{ran}\left({A\upharpoonright }_B\right)=\left\{y|\exists xx\left({A\upharpoonright }_B\right)y\right\}$$
3		brres	$$⊢y\in \mathrm{V}\to \left(x\left({A\upharpoonright }_B\right)y\leftrightarrow \left(x\in B\wedge xAy\right)\right)$$
4	3	elv	$$⊢x\left({A\upharpoonright }_B\right)y\leftrightarrow \left(x\in B\wedge xAy\right)$$
5	4	exbii	$$⊢\exists xx\left({A\upharpoonright }_B\right)y\leftrightarrow \exists x\left(x\in B\wedge xAy\right)$$
6		df-rex	$$⊢\exists x\in BxAy\leftrightarrow \exists x\left(x\in B\wedge xAy\right)$$
7	5 6	bitr4i	$$⊢\exists xx\left({A\upharpoonright }_B\right)y\leftrightarrow \exists x\in BxAy$$
8	7	abbii	$$⊢\left\{y|\exists xx\left({A\upharpoonright }_B\right)y\right\}=\left\{y|\exists x\in BxAy\right\}$$
9	1 2 8	3eqtri	$$⊢A\left[B\right]=\left\{y|\exists x\in BxAy\right\}$$