Theorem forn 5644

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

Syntax hints:   -> wi 4   = wceq 1369   ran crn 4862   Fn wfn 5434   -onto->wfo 5437

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 185  df-an 371  df-fo 5445

This theorem is referenced by:  dffo2  5645  foima  5646  fodmrnu  5649  f1imacnv  5678  foimacnv  5679  foun  5680  resdif  5682  fococnv2  5687  cbvfo  6014  isoini  6050  isofrlem  6052  isoselem  6053  canth  6070  f1opw2  6334  fornex  6567  wemoiso2  6584  curry1  6685  curry2  6688  bren  7340  en1  7397  fopwdom  7440  domss2  7491  mapen  7496  ssenen  7506  phplem4  7514  php3  7518  ssfi  7554  fodomfib  7612  f1opwfi  7636  ordiso2  7750  ordtypelem10  7762  oismo  7775  brwdom  7803  brwdom2  7809  wdomtr  7811  unxpwdom2  7824  wemapwe  7949  wemapweOLD  7950  infxpenc2lem1  8206  fseqen  8218  fodomfi2  8251  infpwfien  8253  infmap2  8408  ackbij2  8433  infpssr  8498  fodomb  8714  fpwwe2lem6  8823  fpwwe2lem9  8826  tskuni  8971  gruen  9000  hashfacen  12228  supcvg  13339  ruclem13  13545  unbenlem  13990  imasval  14470  imasaddfnlem  14487  imasvscafn  14496  imasless  14499  xpsfrn  14528  fulloppc  14853  imasmnd2  15479  imasgrp2  15691  oppglsm  16162  efgrelexlemb  16268  gsumzres  16409  gsumzcl2  16410  gsumzf1o  16412  gsumzresOLD  16413  gsumzclOLD  16414  gsumzf1oOLD  16415  gsumzaddlem  16429  gsumzaddlemOLD  16431  gsumconst  16449  gsumzmhm  16452  gsumzmhmOLD  16453  gsumzoppg  16462  gsumzoppgOLD  16463  dprdf1o  16551  imasrng  16733  gsumfsum  17901  zncyg  18003  znf1o  18006  znleval  18009  znunit  18018  cygznlem2a  18022  indlcim  18291  cmpfi  19033  cnconn  19048  1stcfb  19071  qtopval2  19291  basqtop  19306  tgqtop  19307  imastopn  19315  hmeontr  19364  hmeoqtop  19370  nrmhmph  19389  cmphaushmeo  19395  elfm3  19545  divstgpopn  19712  tsmsf1o  19741  imasf1oxmet  19972  imasf1omet  19973  imasf1oxms  20086  cnheiborlem  20548  ovolctb  20995  dyadmbl  21102  dvcnvrelem2  21512  dvcnvre  21513  efifo  22025  logrn  22032  dvrelog  22104  efopnlem2  22124  fsumdvdsmul  22557  f1otrg  23139  axcontlem10  23241  eupares  23618  eupath2lem3  23622  isgrpo  23705  isgrpoi  23707  isgrp2d  23744  isgrpda  23806  rngopid  23832  opidon2  23833  circgrp  23883  rngmgmbs4  23926  pjrn  25132  ballotlemro  26927  erdsze2lem1  27113  cnpcon  27141  bdayrn  27840  mblfinlem2  28455  volsupnfl  28462  ismtyres  28733  dnnumch2  29424  lnmlmic  29467  pwslnmlem1  29471  pwslnmlem2  29472  stoweidlem27  29848  mapdrn  35390