Theorem forn 6461

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

Syntax hints:   → wi 4   = wceq 1522  ran crn 5444   Fn wfn 6220  –onto→wfo 6223

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 208  df-an 397  df-fo 6231

This theorem is referenced by:  dffo2  6462  foima  6463  fodmrnu  6466  f1imacnv  6499  foimacnv  6500  foun  6501  resdif  6503  fococnv2  6508  foelrni  6595  cbvfo  6910  isoini  6954  isofrlem  6956  isoselem  6957  canth  6974  f1opw2  7258  fornex  7513  wemoiso2  7531  curry1  7655  curry2  7658  bren  8366  en1  8424  fopwdom  8472  domss2  8523  mapen  8528  ssenen  8538  phplem4  8546  php3  8550  ssfi  8584  fodomfib  8644  f1opwfi  8674  ordiso2  8825  ordtypelem10  8837  oismo  8850  brwdom  8877  brwdom2  8883  wdomtr  8885  unxpwdom2  8898  wemapwe  9006  infxpenc2lem1  9291  fseqen  9299  fodomfi2  9332  infpwfien  9334  infmap2  9486  ackbij2  9511  infpssr  9576  fodomb  9794  fpwwe2lem6  9903  fpwwe2lem9  9906  tskuni  10051  gruen  10080  focdmex  13561  hashfacen  13660  supcvg  15044  ruclem13  15428  unbenlem  16073  imasval  16613  imasaddfnlem  16630  imasvscafn  16639  imasless  16642  xpsfrn  16670  fulloppc  17021  imasmnd2  17766  resgrpplusfrn  17875  imasgrp2  17971  oppglsm  18497  efgrelexlemb  18603  gsumzres  18750  gsumzcl2  18751  gsumzf1o  18753  gsumzaddlem  18761  gsumconst  18774  gsumzmhm  18777  gsumzoppg  18784  dprdf1o  18871  imasring  19059  gsumfsum  20294  zncyg  20377  znf1o  20380  znleval  20383  znunit  20392  cygznlem2a  20396  indlcim  20666  cmpfi  21700  cnconn  21714  1stcfb  21737  qtopval2  21988  basqtop  22003  tgqtop  22004  imastopn  22012  hmeontr  22061  hmeoqtop  22067  nrmhmph  22086  cmphaushmeo  22092  elfm3  22242  qustgpopn  22411  tsmsf1o  22436  imasf1oxmet  22668  imasf1omet  22669  imasf1oxms  22782  cnheiborlem  23241  ovolctb  23774  dyadmbl  23884  dvcnvrelem2  24298  dvcnvre  24299  efifo  24812  circgrp  24817  circsubm  24818  logrn  24823  dvrelog  24901  efopnlem2  24921  fsumdvdsmul  25454  f1otrg  26340  axcontlem10  26442  isgrpo  27965  isgrpoi  27966  pjrn  29175  padct  30143  cycpmconjvlem  30420  cycpmconjslem2  30435  imaslmod  30576  qusdimsum  30628  sigapildsys  31038  carsgclctunlem3  31195  ballotlemro  31397  erdsze2lem1  32058  cnpconn  32085  bdayimaon  32806  nosupbday  32814  noetalem3  32828  noetalem4  32829  bdayrn  32854  poimirlem15  34438  mblfinlem2  34461  volsupnfl  34468  ismtyres  34618  rngopidOLD  34663  opidon2OLD  34664  rngmgmbs4  34741  isgrpda  34765  mapdrn  38316  dnnumch2  39130  lnmlmic  39173  pwslnmlem1  39177  pwslnmlem2  39178  ntrneifv2  39915  ssnnf1octb  40996  stoweidlem27  41854  fourierdlem51  41984  fourierdlem102  42035  fourierdlem114  42047  sge0fodjrnlem  42240  nnfoctbdjlem  42279  nnfoctbdj  42280