Theorem forn 5780

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

Syntax hints:   -> wi 4   = wceq 1398   ran crn 4989   Fn wfn 5565   -onto->wfo 5568

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 369  df-fo 5576

This theorem is referenced by:  dffo2  5781  foima  5782  fodmrnu  5785  f1imacnv  5814  foimacnv  5815  foun  5816  resdif  5818  fococnv2  5823  foelrni  5896  cbvfo  6167  isoini  6209  isofrlem  6211  isoselem  6212  canth  6229  f1opw2  6501  fornex  6742  wemoiso2  6759  curry1  6865  curry2  6868  bren  7518  en1  7575  fopwdom  7618  domss2  7669  mapen  7674  ssenen  7684  phplem4  7692  php3  7696  ssfi  7733  fodomfib  7792  f1opwfi  7816  ordiso2  7932  ordtypelem10  7944  oismo  7957  brwdom  7985  brwdom2  7991  wdomtr  7993  unxpwdom2  8006  wemapwe  8130  wemapweOLD  8131  infxpenc2lem1  8387  fseqen  8399  fodomfi2  8432  infpwfien  8434  infmap2  8589  ackbij2  8614  infpssr  8679  fodomb  8895  fpwwe2lem6  9002  fpwwe2lem9  9005  tskuni  9150  gruen  9179  hashfacen  12487  supcvg  13749  ruclem13  14059  unbenlem  14510  imasval  15000  imasaddfnlem  15017  imasvscafn  15026  imasless  15029  xpsfrn  15058  fulloppc  15410  imasmnd2  16156  imasgrp2  16384  oppglsm  16861  efgrelexlemb  16967  gsumzres  17113  gsumzcl2  17114  gsumzf1o  17116  gsumzresOLD  17117  gsumzclOLD  17118  gsumzf1oOLD  17119  gsumzaddlem  17133  gsumzaddlemOLD  17135  gsumconst  17152  gsumzmhm  17155  gsumzmhmOLD  17156  gsumzoppg  17165  gsumzoppgOLD  17166  dprdf1o  17274  imasring  17463  gsumfsum  18679  zncyg  18760  znf1o  18763  znleval  18766  znunit  18775  cygznlem2a  18779  indlcim  19042  cmpfi  20075  cnconn  20089  1stcfb  20112  qtopval2  20363  basqtop  20378  tgqtop  20379  imastopn  20387  hmeontr  20436  hmeoqtop  20442  nrmhmph  20461  cmphaushmeo  20467  elfm3  20617  qustgpopn  20784  tsmsf1o  20813  imasf1oxmet  21044  imasf1omet  21045  imasf1oxms  21158  cnheiborlem  21620  ovolctb  22067  dyadmbl  22175  dvcnvrelem2  22585  dvcnvre  22586  efifo  23100  circgrp  23105  circsubm  23106  logrn  23112  dvrelog  23186  efopnlem2  23206  fsumdvdsmul  23669  f1otrg  24376  axcontlem10  24478  eupares  25177  eupath2lem3  25181  isgrpo  25396  isgrpoi  25398  isgrp2d  25435  isgrpda  25497  rngopidOLD  25523  opidon2OLD  25524  circgrpOLD  25574  rngmgmbs4  25617  pjrn  26823  padct  27776  sigapildsys  28388  carsgclctunlem3  28528  ballotlemro  28725  erdsze2lem1  28911  cnpcon  28939  bdayrn  29677  mblfinlem2  30292  volsupnfl  30299  ismtyres  30544  dnnumch2  31230  lnmlmic  31273  pwslnmlem1  31277  pwslnmlem2  31278  stoweidlem27  32048  fourierdlem51  32179  fourierdlem102  32230  fourierdlem114  32242  mapdrn  37773