Theorem forn 5129

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 4928	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
2	1	simprbi 269	1 |- ( F : A -onto-> B -> ran F = B )

Syntax hints:   -> wi 4   = wceq 1284   ran crn 4364   Fn wfn 4917   -onto->wfo 4920

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

This theorem depends on definitions:  df-bi 115  df-fo 4928

This theorem is referenced by:  dffo2  5130  foima  5131  fodmrnu  5134  f1imacnv  5163  foimacnv  5164  foun  5165  resdif  5168  fococnv2  5172  cbvfo  5445  cbvexfo  5446  isoini  5477  isoselem  5479  f1opw2  5726  fornex  5762  bren  6251  en1  6302  fopwdom  6333  phplem4  6341  phplem4on  6353  ordiso2  6446