Theorem forn 6595

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

Syntax hints:   → wi 4   = wceq 1537  ran crn 5558   Fn wfn 6352  –onto→wfo 6355

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 209  df-an 399  df-fo 6363

This theorem is referenced by:  dffo2  6596  foima  6597  fodmrnu  6600  f1imacnv  6633  foimacnv  6634  foun  6635  resdif  6637  fococnv2  6642  foelrni  6729  cbvfo  7047  isoini  7093  isofrlem  7095  isoselem  7096  canth  7113  f1opw2  7402  fornex  7659  wemoiso2  7677  curry1  7801  curry2  7804  bren  8520  en1  8578  fopwdom  8627  domss2  8678  mapen  8683  ssenen  8693  phplem4  8701  php3  8705  ssfi  8740  fodomfib  8800  f1opwfi  8830  ordiso2  8981  ordtypelem10  8993  oismo  9006  brwdom  9033  brwdom2  9039  wdomtr  9041  unxpwdom2  9054  wemapwe  9162  infxpenc2lem1  9447  fseqen  9455  fodomfi2  9488  infpwfien  9490  infmap2  9642  ackbij2  9667  infpssr  9732  fodomb  9950  fpwwe2lem6  10059  fpwwe2lem9  10062  tskuni  10207  gruen  10236  focdmex  13714  hashfacen  13815  supcvg  15213  ruclem13  15597  unbenlem  16246  imasval  16786  imasaddfnlem  16803  imasvscafn  16812  imasless  16815  xpsfrn  16843  fulloppc  17194  imasmnd2  17950  resgrpplusfrn  18119  imasgrp2  18216  oppglsm  18769  efgrelexlemb  18878  gsumzres  19031  gsumzcl2  19032  gsumzf1o  19034  gsumzaddlem  19043  gsumconst  19056  gsumzmhm  19059  gsumzoppg  19066  dprdf1o  19156  imasring  19371  gsumfsum  20614  zncyg  20697  znf1o  20700  znleval  20703  znunit  20712  cygznlem2a  20716  indlcim  20986  cmpfi  22018  cnconn  22032  1stcfb  22055  qtopval2  22306  basqtop  22321  tgqtop  22322  imastopn  22330  hmeontr  22379  hmeoqtop  22385  nrmhmph  22404  cmphaushmeo  22410  elfm3  22560  qustgpopn  22730  tsmsf1o  22755  imasf1oxmet  22987  imasf1omet  22988  imasf1oxms  23101  cnheiborlem  23560  ovolctb  24093  dyadmbl  24203  dvcnvrelem2  24617  dvcnvre  24618  efifo  25133  circgrp  25138  circsubm  25139  logrn  25144  dvrelog  25222  efopnlem2  25242  fsumdvdsmul  25774  f1otrg  26659  axcontlem10  26761  isgrpo  28276  isgrpoi  28277  pjrn  29486  padct  30457  cycpmconjvlem  30785  cycpmconjslem2  30799  imaslmod  30924  qusdimsum  31026  sigapildsys  31423  carsgclctunlem3  31580  ballotlemro  31782  erdsze2lem1  32452  cnpconn  32479  bdayimaon  33199  nosupbday  33207  noetalem3  33221  noetalem4  33222  bdayrn  33247  poimirlem15  34909  mblfinlem2  34932  volsupnfl  34939  ismtyres  35088  rngopidOLD  35133  opidon2OLD  35134  rngmgmbs4  35211  isgrpda  35235  mapdrn  38787  dnnumch2  39652  lnmlmic  39695  pwslnmlem1  39699  pwslnmlem2  39700  ntrneifv2  40437  ssnnf1octb  41463  stoweidlem27  42319  fourierdlem51  42449  fourierdlem102  42500  fourierdlem114  42512  sge0fodjrnlem  42705  nnfoctbdjlem  42744  nnfoctbdj  42745