Theorem forn 5273

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 4794	. 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 4774   Fn wfn 4777  -onto->wfo 4780

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 4794

This theorem is referenced by:  dffo2  5274  foima  5275  fodmrnu  5278  f1imacnv  5303  foimacnv  5304  resdif  5307  f1ococnv2  5310  dffo4  5424  isoini  5498  bren  6031  enpw1  6063  enmap1lem5  6074  nenpw1pwlem2  6086  ncdisjun  6137  1cnc  6140  sbthlem3  6206