Theorem forn 6742

Description: The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
forn	⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)

Proof of Theorem forn

Step	Hyp	Ref	Expression
1		df-fo 6485	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
2	1	simprbi 497	1 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)

Syntax hints:   → wi 4   = wceq 1540  ran crn 5621   Fn wfn 6474  –onto→wfo 6477

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 206  df-an 397  df-fo 6485

This theorem is referenced by:  dffo2  6743  foima  6744  fodmrnu  6747  focnvimacdmdm  6751  focofo  6752  foco  6753  f1imacnv  6783  foimacnv  6784  foun  6785  resdif  6788  fococnv2  6793  foelcdmi  6887  cbvfo  7217  isoini  7265  isofrlem  7267  isoselem  7268  canth  7290  f1opw2  7586  focdmex  7866  wemoiso2  7885  curry1  8012  curry2  8015  mapfoss  8711  bren  8814  brenOLD  8815  en1  8886  en1OLD  8887  fopwdom  8945  domss2  9001  mapen  9006  ssenen  9016  ssfiALT  9039  phplem2  9073  php3  9077  phplem4OLD  9085  php3OLD  9089  fodomfib  9191  f1opwfi  9221  ordiso2  9372  ordtypelem10  9384  oismo  9397  brwdom  9424  brwdom2  9430  wdomtr  9432  unxpwdom2  9445  wemapwe  9554  infxpenc2lem1  9876  fseqen  9884  fodomfi2  9917  infpwfien  9919  infmap2  10075  ackbij2  10100  infpssr  10165  fodomb  10383  fpwwe2lem5  10492  fpwwe2lem8  10495  tskuni  10640  gruen  10669  hashfacenOLD  14267  supcvg  15667  ruclem13  16050  unbenlem  16706  imasval  17319  imasaddfnlem  17336  imasvscafn  17345  imasless  17348  xpsfrn  17376  fulloppc  17735  imasmnd2  18519  resgrpplusfrn  18689  imasgrp2  18786  oppglsm  19343  efgrelexlemb  19451  gsumzres  19605  gsumzcl2  19606  gsumzf1o  19608  gsumzaddlem  19617  gsumconst  19630  gsumzmhm  19633  gsumzoppg  19640  dprdf1o  19730  imasring  19953  gsumfsum  20771  zncyg  20862  znf1o  20865  znleval  20868  znunit  20877  cygznlem2a  20881  indlcim  21153  cmpfi  22665  cnconn  22679  1stcfb  22702  qtopval2  22953  basqtop  22968  tgqtop  22969  imastopn  22977  hmeontr  23026  hmeoqtop  23032  nrmhmph  23051  cmphaushmeo  23057  elfm3  23207  qustgpopn  23377  tsmsf1o  23402  imasf1oxmet  23634  imasf1omet  23635  imasf1oxms  23751  cnheiborlem  24223  ovolctb  24760  dyadmbl  24870  dvcnvrelem2  25288  dvcnvre  25289  efifo  25809  circgrp  25814  circsubm  25815  logrn  25820  dvrelog  25898  efopnlem2  25918  fsumdvdsmul  26450  bdayimaon  26947  noetasuplem4  26990  noetainflem4  26994  bdayrn  27021  noeta2  27030  f1otrg  27521  axcontlem10  27630  isgrpo  29147  isgrpoi  29148  pjrn  30357  padct  31341  cycpmconjvlem  31695  cycpmconjslem2  31709  imaslmod  31849  qusdimsum  32007  sigapildsys  32428  carsgclctunlem3  32587  ballotlemro  32789  erdsze2lem1  33464  cnpconn  33491  poimirlem15  35905  mblfinlem2  35928  volsupnfl  35935  ismtyres  36079  rngopidOLD  36124  opidon2OLD  36125  rngmgmbs4  36202  isgrpda  36226  mapdrn  39925  riccrng1  40514  dnnumch2  41141  lnmlmic  41184  pwslnmlem1  41188  pwslnmlem2  41189  ntrneifv2  42019  ssnnf1octb  43068  stoweidlem27  43912  fourierdlem51  44042  fourierdlem102  44093  fourierdlem114  44105  sge0fodjrnlem  44299  nnfoctbdjlem  44338  nnfoctbdj  44339