Theorem forn 5421

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

Syntax hints:   -> wi 4   = wceq 1348   ran crn 4610   Fn wfn 5191   -onto->wfo 5194

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

This theorem depends on definitions:  df-bi 116  df-fo 5202

This theorem is referenced by:  dffo2  5422  foima  5423  fodmrnu  5426  f1imacnv  5457  foimacnv  5458  foun  5459  resdif  5462  fococnv2  5466  cbvfo  5762  cbvexfo  5763  isoini  5795  isoselem  5797  canth  5805  f1opw2  6053  fornex  6092  bren  6723  en1  6775  fopwdom  6812  mapen  6822  ssenen  6827  phplem4  6831  phplem4on  6843  ordiso2  7010  djuunr  7041  focdmex  10714  hashfacen  10764  ennnfonelemrn  12367  hmeontr  13072