Theorem forn 6824

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

Syntax hints:   → wi 4   = wceq 1537  ran crn 5690   Fn wfn 6558  –onto→wfo 6561

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 207  df-an 396  df-fo 6569

This theorem is referenced by:  dffo2  6825  foima  6826  fodmrnu  6829  focnvimacdmdm  6833  focofo  6834  foco  6835  f1imacnv  6865  foimacnv  6866  foun  6867  resdif  6870  fococnv2  6875  foelcdmi  6970  f1ounsn  7292  cbvfo  7309  f1ocoima  7323  isoini  7358  isofrlem  7360  isoselem  7361  canth  7385  f1opw2  7688  focdmex  7979  wemoiso2  7998  curry1  8128  curry2  8131  mapfoss  8891  bren  8994  en1  9063  fopwdom  9119  domss2  9175  mapen  9180  ssenen  9190  ssfiALT  9213  phplem2  9243  php3  9247  phplem4OLD  9255  php3OLD  9259  fodomfib  9367  fodomfibOLD  9369  f1opwfi  9394  ordiso2  9553  ordtypelem10  9565  oismo  9578  brwdom  9605  brwdom2  9611  wdomtr  9613  unxpwdom2  9626  wemapwe  9735  infxpenc2lem1  10057  fseqen  10065  fodomfi2  10098  infpwfien  10100  infmap2  10255  ackbij2  10280  infpssr  10346  fodomb  10564  fpwwe2lem5  10673  fpwwe2lem8  10676  tskuni  10821  gruen  10850  supcvg  15889  ruclem13  16275  unbenlem  16942  imasval  17558  imasaddfnlem  17575  imasvscafn  17584  imasless  17587  xpsfrn  17615  fulloppc  17976  imasmnd2  18800  resgrpplusfrn  18981  imasgrp2  19086  oppglsm  19675  efgrelexlemb  19783  gsumzres  19942  gsumzcl2  19943  gsumzf1o  19945  gsumzaddlem  19954  gsumconst  19967  gsumzmhm  19970  gsumzoppg  19977  dprdf1o  20067  imasrng  20195  imasring  20344  gsumfsum  21470  zncyg  21585  znf1o  21588  znleval  21591  znunit  21600  cygznlem2a  21604  indlcim  21878  cmpfi  23432  cnconn  23446  1stcfb  23469  qtopval2  23720  basqtop  23735  tgqtop  23736  imastopn  23744  hmeontr  23793  hmeoqtop  23799  nrmhmph  23818  cmphaushmeo  23824  elfm3  23974  qustgpopn  24144  tsmsf1o  24169  imasf1oxmet  24401  imasf1omet  24402  imasf1oxms  24518  cnheiborlem  25000  ovolctb  25539  dyadmbl  25649  dvcnvrelem2  26072  dvcnvre  26073  efifo  26604  circgrp  26609  circsubm  26610  logrn  26615  dvrelog  26694  efopnlem2  26714  fsumdvdsmul  27253  fsumdvdsmulOLD  27255  bdayimaon  27753  noetasuplem4  27796  noetainflem4  27800  bdayrn  27835  noeta2  27844  negsunif  28102  negsbdaylem  28103  zssno  28382  f1otrg  28894  axcontlem10  29003  isgrpo  30526  isgrpoi  30527  pjrn  31736  padct  32737  cycpmconjvlem  33144  cycpmconjslem2  33158  imaslmod  33361  qusdimsum  33656  sigapildsys  34143  carsgclctunlem3  34302  ballotlemro  34504  erdsze2lem1  35188  cnpconn  35215  poimirlem15  37622  mblfinlem2  37645  volsupnfl  37652  ismtyres  37795  rngopidOLD  37840  opidon2OLD  37841  rngmgmbs4  37918  isgrpda  37942  mapdrn  41632  ricdrng1  42515  dnnumch2  43034  lnmlmic  43077  pwslnmlem1  43081  pwslnmlem2  43082  ntrneifv2  44070  ssnnf1octb  45137  stoweidlem27  45983  fourierdlem51  46113  fourierdlem102  46164  fourierdlem114  46176  sge0fodjrnlem  46372  nnfoctbdjlem  46411  nnfoctbdj  46412  3f1oss1  47025  uspgrimprop  47811