Theorem forn 6797

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5652   Fn wfn 6532  –onto→wfo 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fo 6543

This theorem is used by:  dffo2  6798  foima  6799  fodmrnu  6802  focnvimacdmdm  6806  focofo  6807  foco  6808  f1imacnv  6839  foimacnv  6840  foun  6841  resdif  6844  fococnv2  6849  foelcdmi  6944  f1ounsn  7278  cbvfo  7295  f1ocoima  7309  isoini  7344  isofrlem  7346  isoselem  7347  canth  7372  f1opw2  7674  focdmex  7966  wemoiso2  7984  curry1  8113  curry2  8116  mapfoss  8867  bren  8976  en1  9044  fopwdom  9097  domss2  9148  mapen  9153  ssenen  9163  ssfiALT  9182  phplem2  9213  php3  9217  fodomfib  9313  f1opwfi  9338  ordiso2  9502  ordtypelem10  9514  oismo  9527  brwdom  9554  brwdom2  9560  wdomtr  9562  unxpwdom2  9575  wemapwe  9691  infxpenc2lem1  10091  fseqen  10099  fodomfi2  10132  infpwfien  10134  infmap2  10288  ackbij2  10313  infpssr  10379  fodomb  10598  fpwwe2lem5  10713  fpwwe2lem8  10716  tskuni  10861  gruen  10890  supcvg  16018  ruclem13  16403  unbenlem  17079  imasval  17676  imasaddfnlem  17693  imasvscafn  17702  imasless  17705  xpsfrn  17733  fulloppc  18092  mgmidprnd  18851  imasmgm2  18856  imasmnd2  18961  resgrpplusfrn  19154  imasgrp2  19258  oppglsm  19849  efgrelexlemb  19957  gsumzres  20116  gsumzcl2  20117  gsumzf1o  20119  gsumzaddlem  20128  gsumconst  20141  gsumzmhm  20144  gsumzoppg  20151  dprdf1o  20241  imasrng  20392  imasring  20553  gsumfsum  21733  zncyg  21847  znf1o  21850  znleval  21853  znunit  21862  cygznlem2a  21866  indlcim  22139  cmpfi  23719  cnconn  23733  1stcfb  23756  qtopval2  24008  basqtop  24023  tgqtop  24024  imastopn  24032  hmeontr  24081  hmeoqtop  24087  nrmhmph  24106  cmphaushmeo  24112  elfm3  24262  qustgpopn  24432  tsmsf1o  24457  imasf1oxmet  24687  imasf1omet  24688  imasf1oxms  24801  cnheiborlem  25268  ovolctb  25804  dyadmbl  25914  dvcnvrelem2  26331  dvcnvre  26332  efifo  26868  circgrp  26873  circsubm  26874  logrn  26879  dvrelog  26958  efopnlem2  26978  fsumdvdsmul  27515  bdayimaon  28043  noetasuplem4  28086  noetainflem4  28090  bdayrn  28130  noeta2  28140  negsunif  28434  negbdaylem  28435  zssno  28760  f1otrg  29441  axcontlem10  29544  isgrpo  31092  isgrpoi  31093  pjrn  32302  padct  33303  cycpmconjvlem  33695  cycpmconjslem2  33709  imaslmod  33907  esplysply  34196  qusdimsum  34253  sigapildsys  34788  carsgclctunlem3  34945  ballotlemro  35148  onvfowev  35878  erdsze2lem1  35947  cnpconn  35974  poimirlem15  38533  mblfinlem2  38556  volsupnfl  38563  ismtyres  38722  rngopidOLD  38767  opidon2OLD  38768  rngmgmbs4  38845  isgrpda  38869  mapdrn  42686  ricdrng1  43572  dnnumch2  44031  lnmlmic  44074  pwslnmlem1  44078  pwslnmlem2  44079  ntrneifv2  45065  ssnnf1octb  46178  stoweidlem27  47006  fourierdlem51  47136  fourierdlem102  47187  fourierdlem114  47199  sge0fodjrnlem  47395  nnfoctbdjlem  47434  nnfoctbdj  47435  3f1oss1  48114  fonex  49946  tposres3  49958