Theorem forn 5784

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 5580	. 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 1381   ran crn 4986   Fn wfn 5569   -onto->wfo 5572

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 5580

This theorem is referenced by:  dffo2  5785  foima  5786  fodmrnu  5789  f1imacnv  5818  foimacnv  5819  foun  5820  resdif  5822  fococnv2  5827  foelrni  5902  cbvfo  6173  isoini  6215  isofrlem  6217  isoselem  6218  canth  6235  f1opw2  6509  fornex  6750  wemoiso2  6767  curry1  6873  curry2  6876  bren  7523  en1  7580  fopwdom  7623  domss2  7674  mapen  7679  ssenen  7689  phplem4  7697  php3  7701  ssfi  7738  fodomfib  7798  f1opwfi  7822  ordiso2  7938  ordtypelem10  7950  oismo  7963  brwdom  7991  brwdom2  7997  wdomtr  7999  unxpwdom2  8012  wemapwe  8137  wemapweOLD  8138  infxpenc2lem1  8394  fseqen  8406  fodomfi2  8439  infpwfien  8441  infmap2  8596  ackbij2  8621  infpssr  8686  fodomb  8902  fpwwe2lem6  9011  fpwwe2lem9  9014  tskuni  9159  gruen  9188  hashfacen  12477  supcvg  13641  ruclem13  13847  unbenlem  14298  imasval  14780  imasaddfnlem  14797  imasvscafn  14806  imasless  14809  xpsfrn  14838  fulloppc  15160  imasmnd2  15826  imasgrp2  16054  oppglsm  16531  efgrelexlemb  16637  gsumzres  16783  gsumzcl2  16784  gsumzf1o  16786  gsumzresOLD  16787  gsumzclOLD  16788  gsumzf1oOLD  16789  gsumzaddlem  16803  gsumzaddlemOLD  16805  gsumconst  16823  gsumzmhm  16826  gsumzmhmOLD  16827  gsumzoppg  16836  gsumzoppgOLD  16837  dprdf1o  16947  imasring  17136  gsumfsum  18352  zncyg  18454  znf1o  18457  znleval  18460  znunit  18469  cygznlem2a  18473  indlcim  18742  cmpfi  19774  cnconn  19789  1stcfb  19812  qtopval2  20063  basqtop  20078  tgqtop  20079  imastopn  20087  hmeontr  20136  hmeoqtop  20142  nrmhmph  20161  cmphaushmeo  20167  elfm3  20317  qustgpopn  20484  tsmsf1o  20513  imasf1oxmet  20744  imasf1omet  20745  imasf1oxms  20858  cnheiborlem  21320  ovolctb  21767  dyadmbl  21875  dvcnvrelem2  22285  dvcnvre  22286  efifo  22799  circgrp  22804  circsubm  22805  logrn  22811  dvrelog  22883  efopnlem2  22903  fsumdvdsmul  23336  f1otrg  24039  axcontlem10  24141  eupares  24840  eupath2lem3  24844  isgrpo  25063  isgrpoi  25065  isgrp2d  25102  isgrpda  25164  rngopidOLD  25190  opidon2OLD  25191  circgrpOLD  25241  rngmgmbs4  25284  pjrn  26490  ballotlemro  28327  erdsze2lem1  28513  cnpcon  28541  bdayrn  29405  mblfinlem2  30020  volsupnfl  30027  ismtyres  30272  dnnumch2  30959  lnmlmic  31002  pwslnmlem1  31006  pwslnmlem2  31007  stoweidlem27  31694  fourierdlem51  31825  fourierdlem102  31876  fourierdlem114  31888  mapdrn  37078