Metamath Proof Explorer

Theorem foima

Description: The image of the domain of an onto function. (Contributed by NM, 29-Nov-2002)

Ref Expression
Assertion foima 
|- ( F : A -onto-> B -> ( F " A ) = B )

Proof

Step Hyp Ref Expression
1 imadmrn 
 |-  ( F " dom F ) = ran F
2 fof 
 |-  ( F : A -onto-> B -> F : A --> B )
3 2 fdmd 
 |-  ( F : A -onto-> B -> dom F = A )
4 3 imaeq2d 
 |-  ( F : A -onto-> B -> ( F " dom F ) = ( F " A ) )
5 forn 
 |-  ( F : A -onto-> B -> ran F = B )
6 1 4 5 3eqtr3a 
 |-  ( F : A -onto-> B -> ( F " A ) = B )