Theorem forn 5236

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 5021	. 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 1289   ran crn 4439   Fn wfn 5010   -onto->wfo 5013

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 5021

This theorem is referenced by:  dffo2  5237  foima  5238  fodmrnu  5241  f1imacnv  5270  foimacnv  5271  foun  5272  resdif  5275  fococnv2  5279  cbvfo  5564  cbvexfo  5565  isoini  5597  isoselem  5599  f1opw2  5850  fornex  5886  bren  6464  en1  6516  fopwdom  6552  mapen  6562  ssenen  6567  phplem4  6571  phplem4on  6583  ordiso2  6728  djuunr  6758  focdmex  10195  hashfacen  10241