Metamath Proof Explorer


Theorem forn

Description: The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994)

Ref Expression
Assertion forn F : A onto B ran F = B

Proof

Step Hyp Ref Expression
1 df-fo F : A onto B F Fn A ran F = B
2 1 simprbi F : A onto B ran F = B