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 )