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

Metamath Proof Explorer

Theorem dfimafn2

Description: Alternate definition of the image of a function as an indexed union of singletons of function values. (Contributed by Raph Levien, 20-Nov-2006)

Ref Expression
Assertion dfimafn2 
|- ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = U_ x e. A { ( F ` x ) } )

Proof

Step Hyp Ref Expression
1 dfimafn 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = { y | E. x e. A ( F ` x ) = y } )
2 iunab 
 |-  U_ x e. A { y | ( F ` x ) = y } = { y | E. x e. A ( F ` x ) = y }
3 1 2 eqtr4di 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = U_ x e. A { y | ( F ` x ) = y } )
4 df-sn 
 |-  { ( F ` x ) } = { y | y = ( F ` x ) }
5 eqcom 
 |-  ( y = ( F ` x ) <-> ( F ` x ) = y )
6 5 abbii 
 |-  { y | y = ( F ` x ) } = { y | ( F ` x ) = y }
7 4 6 eqtri 
 |-  { ( F ` x ) } = { y | ( F ` x ) = y }
8 7 a1i 
 |-  ( x e. A -> { ( F ` x ) } = { y | ( F ` x ) = y } )
9 8 iuneq2i 
 |-  U_ x e. A { ( F ` x ) } = U_ x e. A { y | ( F ` x ) = y }
10 3 9 eqtr4di 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = U_ x e. A { ( F ` x ) } )