Theorem forn 5615

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

Syntax hints:   -> wi 4   = wceq 1649   ran crn 4838   Fn wfn 5408   -onto->wfo 5411

This theorem is referenced by:  dffo2  5616  foima  5617  fodmrnu  5620  f1imacnv  5650  foimacnv  5651  foun  5652  resdif  5655  fococnv2  5660  fornex  5929  cbvfo  5981  isoini  6017  isofrlem  6019  isoselem  6020  wemoiso2  6038  f1opw2  6257  curry1  6397  curry2  6400  canth  6498  bren  7076  en1  7133  fopwdom  7175  domss2  7225  mapen  7230  ssenen  7240  phplem4  7248  php3  7252  ssfi  7288  fodomfib  7345  f1opwfi  7368  ordiso2  7440  ordtypelem10  7452  oismo  7465  brwdom  7491  brwdom2  7497  wdomtr  7499  unxpwdom2  7512  wemapwe  7610  infxpenc2lem1  7856  fseqen  7864  fodomfi2  7897  infpwfien  7899  infmap2  8054  ackbij2  8079  infpssr  8144  fodomb  8360  fpwwe2lem6  8466  fpwwe2lem9  8469  tskuni  8614  gruen  8643  hashfacen  11658  supcvg  12590  ruclem13  12796  unbenlem  13231  imasval  13692  imasaddfnlem  13708  imasvscafn  13717  imasless  13720  xpsfrn  13749  fulloppc  14074  imasmnd2  14687  imasgrp2  14888  oppglsm  15231  efgrelexlemb  15337  gsumzres  15472  gsumzcl  15473  gsumzf1o  15474  gsumzaddlem  15481  gsumconst  15487  gsumzmhm  15488  gsumzoppg  15494  dprdf1o  15545  imasrng  15680  gsumfsum  16721  zncyg  16784  znf1o  16787  znleval  16790  znunit  16799  cygznlem2a  16803  cmpfi  17425  cnconn  17438  1stcfb  17461  qtopval2  17681  basqtop  17696  tgqtop  17697  imastopn  17705  hmeontr  17754  hmeoqtop  17760  nrmhmph  17779  cmphaushmeo  17785  elfm3  17935  divstgpopn  18102  tsmsf1o  18127  imasf1oxmet  18358  imasf1omet  18359  imasf1oxms  18472  cnheiborlem  18932  ovolctb  19339  dyadmbl  19445  dvcnvrelem2  19855  dvcnvre  19856  efifo  20402  logrn  20409  dvrelog  20481  efopnlem2  20501  fsumdvdsmul  20933  eupares  21650  eupath2lem3  21654  isgrpo  21737  isgrpoi  21739  isgrp2d  21776  isgrpda  21838  rngopid  21864  opidon2  21865  circgrp  21915  rngmgmbs4  21958  pjrn  23162  ballotlemro  24733  erdsze2lem1  24842  cnpcon  24870  bdayrn  25545  axcontlem10  25816  mblfinlem  26143  volsupnfl  26150  ismtyres  26407  dnnumch2  27010  lnmlmic  27054  pwslnmlem1  27062  pwslnmlem2  27063  indlcim  27178  stoweidlem27  27643  mapdrn  32132

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

This theorem depends on definitions:  df-bi 178  df-an 361  df-fo 5419