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 | E. x e. B x A y }

Proof

Step	Hyp	Ref	Expression
1		df-ima	|- ( A " B ) = ran ( A |` B )
2		dfrn2	|- ran ( A |` B ) = { y | E. x x ( A |` B ) y }
3		brres	|- ( y e. _V -> ( x ( A |` B ) y <-> ( x e. B /\ x A y ) ) )
4	3	elv	|- ( x ( A |` B ) y <-> ( x e. B /\ x A y ) )
5	4	exbii	|- ( E. x x ( A |` B ) y <-> E. x ( x e. B /\ x A y ) )
6		df-rex	|- ( E. x e. B x A y <-> E. x ( x e. B /\ x A y ) )
7	5 6	bitr4i	|- ( E. x x ( A |` B ) y <-> E. x e. B x A y )
8	7	abbii	|- { y | E. x x ( A |` B ) y } = { y | E. x e. B x A y }
9	1 2 8	3eqtri	|- ( A " B ) = { y | E. x e. B x A y }