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 | 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 }