Theorem forn 6792

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5656   Fn wfn 6528  –onto→wfo 6531

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 6539

This theorem is used by:  dffo2  6793  foima  6794  fodmrnu  6797  focnvimacdmdm  6801  focofo  6802  foco  6803  f1imacnv  6834  foimacnv  6835  foun  6836  resdif  6839  fococnv2  6844  foelcdmi  6939  f1ounsn  7273  cbvfo  7290  f1ocoima  7304  isoini  7339  isofrlem  7341  isoselem  7342  canth  7367  f1opw2  7669  focdmex  7953  wemoiso2  7971  curry1  8101  curry2  8104  mapfoss  8853  bren  8962  en1  9030  fopwdom  9083  domss2  9134  mapen  9139  ssenen  9149  ssfiALT  9168  phplem2  9199  php3  9203  fodomfib  9298  f1opwfi  9323  ordiso2  9487  ordtypelem10  9499  oismo  9512  brwdom  9539  brwdom2  9545  wdomtr  9547  unxpwdom2  9560  wemapwe  9676  infxpenc2lem1  10022  fseqen  10030  fodomfi2  10063  infpwfien  10065  infmap2  10219  ackbij2  10244  infpssr  10310  fodomb  10529  fpwwe2lem5  10644  fpwwe2lem8  10647  tskuni  10792  gruen  10821  supcvg  15945  ruclem13  16330  unbenlem  17000  imasval  17597  imasaddfnlem  17614  imasvscafn  17623  imasless  17626  xpsfrn  17654  fulloppc  18013  mgmidprnd  18771  imasmgm2  18776  imasmnd2  18881  resgrpplusfrn  19074  imasgrp2  19178  oppglsm  19769  efgrelexlemb  19877  gsumzres  20036  gsumzcl2  20037  gsumzf1o  20039  gsumzaddlem  20048  gsumconst  20061  gsumzmhm  20064  gsumzoppg  20071  dprdf1o  20161  imasrng  20312  imasring  20471  gsumfsum  21647  zncyg  21761  znf1o  21764  znleval  21767  znunit  21776  cygznlem2a  21780  indlcim  22053  cmpfi  23633  cnconn  23647  1stcfb  23670  qtopval2  23922  basqtop  23937  tgqtop  23938  imastopn  23946  hmeontr  23995  hmeoqtop  24001  nrmhmph  24020  cmphaushmeo  24026  elfm3  24176  qustgpopn  24346  tsmsf1o  24371  imasf1oxmet  24601  imasf1omet  24602  imasf1oxms  24715  cnheiborlem  25182  ovolctb  25718  dyadmbl  25828  dvcnvrelem2  26245  dvcnvre  26246  efifo  26784  circgrp  26789  circsubm  26790  logrn  26795  dvrelog  26874  efopnlem2  26894  fsumdvdsmul  27431  bdayimaon  27929  noetasuplem4  27972  noetainflem4  27976  bdayrn  28016  noeta2  28026  negsunif  28320  negbdaylem  28321  zssno  28646  f1otrg  29327  axcontlem10  29430  isgrpo  30978  isgrpoi  30979  pjrn  32188  padct  33189  cycpmconjvlem  33581  cycpmconjslem2  33595  imaslmod  33793  esplysply  34081  qusdimsum  34138  sigapildsys  34673  carsgclctunlem3  34831  ballotlemro  35034  onvfowev  35713  erdsze2lem1  35782  cnpconn  35809  poimirlem15  38384  mblfinlem2  38407  volsupnfl  38414  ismtyres  38558  rngopidOLD  38603  opidon2OLD  38604  rngmgmbs4  38681  isgrpda  38705  mapdrn  42522  ricdrng1  43410  dnnumch2  43886  lnmlmic  43929  pwslnmlem1  43933  pwslnmlem2  43934  ntrneifv2  44920  ssnnf1octb  46026  stoweidlem27  46855  fourierdlem51  46985  fourierdlem102  47036  fourierdlem114  47048  sge0fodjrnlem  47244  nnfoctbdjlem  47283  nnfoctbdj  47284  3f1oss1  47963  fonex  49795  tposres3  49807