Theorem forn 5598

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

Syntax hints:   -> wi 4   = wceq 1398   ran crn 4755   Fn wfn 5352   -onto->wfo 5355

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

This theorem depends on definitions:  df-bi 117  df-fo 5363

This theorem is referenced by:  dffo2  5599  foima  5600  fodmrnu  5603  f1imacnv  5636  foimacnv  5637  foun  5638  resdif  5641  fococnv2  5645  foelcdmi  5734  cbvfo  5964  cbvexfo  5965  isoini  5997  isoselem  5999  canth  6009  f1opw2  6269  focdmex  6317  bren  6996  en1  7052  fopwdom  7102  mapen  7112  ssenen  7118  phplem4  7122  phplem4on  7135  ordiso2  7339  djuunr  7370  hashfacen  11233  ballotfilemro  13210  ennnfonelemrn  13254  imasival  13570  imasaddfnlemg  13578  xpsfrn  13614  imasmnd2  13707  imasgrp2  13863  imasrng  14195  imasring  14307  znf1o  14925  znleval  14927  znunit  14933  hmeontr  15304  fsumdvdsmul  15985