Theorem forn 6806

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 6547	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
2	1	simprbi 498	1 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)

Syntax hints:   → wi 4   = wceq 1542  ran crn 5677   Fn wfn 6536  –onto→wfo 6539

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 398  df-fo 6547

This theorem is referenced by:  dffo2  6807  foima  6808  fodmrnu  6811  focnvimacdmdm  6815  focofo  6816  foco  6817  f1imacnv  6847  foimacnv  6848  foun  6849  resdif  6852  fococnv2  6857  foelcdmi  6951  cbvfo  7284  isoini  7332  isofrlem  7334  isoselem  7335  canth  7359  f1opw2  7658  focdmex  7939  wemoiso2  7958  curry1  8087  curry2  8090  mapfoss  8843  bren  8946  brenOLD  8947  en1  9018  en1OLD  9019  fopwdom  9077  domss2  9133  mapen  9138  ssenen  9148  ssfiALT  9171  phplem2  9205  php3  9209  phplem4OLD  9217  php3OLD  9221  fodomfib  9323  f1opwfi  9353  ordiso2  9507  ordtypelem10  9519  oismo  9532  brwdom  9559  brwdom2  9565  wdomtr  9567  unxpwdom2  9580  wemapwe  9689  infxpenc2lem1  10011  fseqen  10019  fodomfi2  10052  infpwfien  10054  infmap2  10210  ackbij2  10235  infpssr  10300  fodomb  10518  fpwwe2lem5  10627  fpwwe2lem8  10630  tskuni  10775  gruen  10804  hashfacenOLD  14411  supcvg  15799  ruclem13  16182  unbenlem  16838  imasval  17454  imasaddfnlem  17471  imasvscafn  17480  imasless  17483  xpsfrn  17511  fulloppc  17870  imasmnd2  18659  resgrpplusfrn  18833  imasgrp2  18935  oppglsm  19505  efgrelexlemb  19613  gsumzres  19772  gsumzcl2  19773  gsumzf1o  19775  gsumzaddlem  19784  gsumconst  19797  gsumzmhm  19800  gsumzoppg  19807  dprdf1o  19897  imasring  20137  gsumfsum  21005  zncyg  21096  znf1o  21099  znleval  21102  znunit  21111  cygznlem2a  21115  indlcim  21387  cmpfi  22904  cnconn  22918  1stcfb  22941  qtopval2  23192  basqtop  23207  tgqtop  23208  imastopn  23216  hmeontr  23265  hmeoqtop  23271  nrmhmph  23290  cmphaushmeo  23296  elfm3  23446  qustgpopn  23616  tsmsf1o  23641  imasf1oxmet  23873  imasf1omet  23874  imasf1oxms  23990  cnheiborlem  24462  ovolctb  24999  dyadmbl  25109  dvcnvrelem2  25527  dvcnvre  25528  efifo  26048  circgrp  26053  circsubm  26054  logrn  26059  dvrelog  26137  efopnlem2  26157  fsumdvdsmul  26689  bdayimaon  27186  noetasuplem4  27229  noetainflem4  27233  bdayrn  27267  noeta2  27276  negsunif  27519  negsbdaylem  27520  f1otrg  28112  axcontlem10  28221  isgrpo  29738  isgrpoi  29739  pjrn  30948  padct  31932  cycpmconjvlem  32288  cycpmconjslem2  32302  imaslmod  32457  qusdimsum  32702  sigapildsys  33149  carsgclctunlem3  33308  ballotlemro  33510  erdsze2lem1  34183  cnpconn  34210  poimirlem15  36492  mblfinlem2  36515  volsupnfl  36522  ismtyres  36665  rngopidOLD  36710  opidon2OLD  36711  rngmgmbs4  36788  isgrpda  36812  mapdrn  40509  ricdrng1  41100  dnnumch2  41773  lnmlmic  41816  pwslnmlem1  41820  pwslnmlem2  41821  ntrneifv2  42817  ssnnf1octb  43879  stoweidlem27  44730  fourierdlem51  44860  fourierdlem102  44911  fourierdlem114  44923  sge0fodjrnlem  45119  nnfoctbdjlem  45158  nnfoctbdj  45159  imasrng  46665