Theorem forn 6118

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

Syntax hints:   -> wi 4   = wceq 1483   ran crn 5115   Fn wfn 5883   -onto->wfo 5886

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 197  df-an 386  df-fo 5894

This theorem is referenced by:  dffo2  6119  foima  6120  fodmrnu  6123  f1imacnv  6153  foimacnv  6154  foun  6155  resdif  6157  fococnv2  6162  foelrni  6244  cbvfo  6544  isoini  6588  isofrlem  6590  isoselem  6591  canth  6608  f1opw2  6888  fornex  7135  wemoiso2  7154  curry1  7269  curry2  7272  bren  7964  en1  8023  fopwdom  8068  domss2  8119  mapen  8124  ssenen  8134  phplem4  8142  php3  8146  ssfi  8180  fodomfib  8240  f1opwfi  8270  ordiso2  8420  ordtypelem10  8432  oismo  8445  brwdom  8472  brwdom2  8478  wdomtr  8480  unxpwdom2  8493  wemapwe  8594  infxpenc2lem1  8842  fseqen  8850  fodomfi2  8883  infpwfien  8885  infmap2  9040  ackbij2  9065  infpssr  9130  fodomb  9348  fpwwe2lem6  9457  fpwwe2lem9  9460  tskuni  9605  gruen  9634  focdmex  13139  hashfacen  13238  supcvg  14588  ruclem13  14971  unbenlem  15612  imasval  16171  imasaddfnlem  16188  imasvscafn  16197  imasless  16200  xpsfrn  16229  fulloppc  16582  imasmnd2  17327  resgrpplusfrn  17436  imasgrp2  17530  oppglsm  18057  efgrelexlemb  18163  gsumzres  18310  gsumzcl2  18311  gsumzf1o  18313  gsumzaddlem  18321  gsumconst  18334  gsumzmhm  18337  gsumzoppg  18344  dprdf1o  18431  imasring  18619  gsumfsum  19813  zncyg  19897  znf1o  19900  znleval  19903  znunit  19912  cygznlem2a  19916  indlcim  20179  cmpfi  21211  cnconn  21225  1stcfb  21248  qtopval2  21499  basqtop  21514  tgqtop  21515  imastopn  21523  hmeontr  21572  hmeoqtop  21578  nrmhmph  21597  cmphaushmeo  21603  elfm3  21754  qustgpopn  21923  tsmsf1o  21948  imasf1oxmet  22180  imasf1omet  22181  imasf1oxms  22294  cnheiborlem  22753  ovolctb  23258  dyadmbl  23368  dvcnvrelem2  23781  dvcnvre  23782  efifo  24293  circgrp  24298  circsubm  24299  logrn  24305  dvrelog  24383  efopnlem2  24403  fsumdvdsmul  24921  f1otrg  25751  axcontlem10  25853  isgrpo  27351  isgrpoi  27352  pjrn  28566  padct  29497  sigapildsys  30225  carsgclctunlem3  30382  ballotlemro  30584  erdsze2lem1  31185  cnpconn  31212  bdayimaon  31843  nosupbday  31851  noetalem3  31865  noetalem4  31866  bdayrn  31891  poimirlem15  33424  mblfinlem2  33447  volsupnfl  33454  ismtyres  33607  rngopidOLD  33652  opidon2OLD  33653  rngmgmbs4  33730  isgrpda  33754  mapdrn  36938  dnnumch2  37615  lnmlmic  37658  pwslnmlem1  37662  pwslnmlem2  37663  ntrneifv2  38378  ssnnf1octb  39382  stoweidlem27  40244  fourierdlem51  40374  fourierdlem102  40425  fourierdlem114  40437  sge0fodjrnlem  40633  nnfoctbdjlem  40672  nnfoctbdj  40673