Theorem forn 5272

Description: The codomain of an onto function is its range. (Contributed by set.mm contributors, 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 4793	. 2 ⊢ (F:A–onto→B ↔ (F Fn A ∧ ran F = B))
2	1	simprbi 450	1 ⊢ (F:A–onto→B → ran F = B)

Syntax hints:   → wi 4   = wceq 1642  ran crn 4773   Fn wfn 4776  –onto→wfo 4779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360  df-fo 4793

This theorem is referenced by:  dffo2  5273  foima  5274  fodmrnu  5277  f1imacnv  5302  foimacnv  5303  resdif  5306  f1ococnv2  5309  dffo4  5423  isoini  5497  bren  6030  enpw1  6062  enmap1lem5  6073  nenpw1pwlem2  6085  ncdisjun  6136  1cnc  6139  sbthlem3  6205