Theorem forn 5109

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

Assertion

Ref	Expression
forn	|- ( F : A -onto-> B -> ran F = B )

Proof of Theorem forn

Step	Hyp	Ref	Expression
1		df-fo 4908	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
2	1	simprbi 260	1 |- ( F : A -onto-> B -> ran F = B )

Syntax hints:   -> wi 4   = wceq 1243   ran crn 4346   Fn wfn 4897   -onto->wfo 4900

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100

This theorem depends on definitions:  df-bi 110  df-fo 4908

This theorem is referenced by:  dffo2  5110  foima  5111  fodmrnu  5114  f1imacnv  5143  foimacnv  5144  foun  5145  resdif  5148  fococnv2  5152  cbvfo  5425  cbvexfo  5426  isoini  5457  isoselem  5459  f1opw2  5706  fornex  5742  bren  6228  en1  6279  fopwdom  6310  phplem4  6318  phplem4on  6329  ordiso2  6357