Theorem forn 6778

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

Syntax hints:   → wi 4   = wceq 1540  ran crn 5642   Fn wfn 6509  –onto→wfo 6512

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 6520

This theorem is referenced by:  dffo2  6779  foima  6780  fodmrnu  6783  focnvimacdmdm  6787  focofo  6788  foco  6789  f1imacnv  6819  foimacnv  6820  foun  6821  resdif  6824  fococnv2  6829  foelcdmi  6925  f1ounsn  7250  cbvfo  7267  f1ocoima  7281  isoini  7316  isofrlem  7318  isoselem  7319  canth  7344  f1opw2  7647  focdmex  7937  wemoiso2  7956  curry1  8086  curry2  8089  mapfoss  8828  bren  8931  en1  8998  fopwdom  9054  domss2  9106  mapen  9111  ssenen  9121  ssfiALT  9144  phplem2  9175  php3  9179  fodomfib  9287  fodomfibOLD  9289  f1opwfi  9314  ordiso2  9475  ordtypelem10  9487  oismo  9500  brwdom  9527  brwdom2  9533  wdomtr  9535  unxpwdom2  9548  wemapwe  9657  infxpenc2lem1  9979  fseqen  9987  fodomfi2  10020  infpwfien  10022  infmap2  10177  ackbij2  10202  infpssr  10268  fodomb  10486  fpwwe2lem5  10595  fpwwe2lem8  10598  tskuni  10743  gruen  10772  supcvg  15829  ruclem13  16217  unbenlem  16886  imasval  17481  imasaddfnlem  17498  imasvscafn  17507  imasless  17510  xpsfrn  17538  fulloppc  17893  imasmnd2  18708  resgrpplusfrn  18889  imasgrp2  18994  oppglsm  19579  efgrelexlemb  19687  gsumzres  19846  gsumzcl2  19847  gsumzf1o  19849  gsumzaddlem  19858  gsumconst  19871  gsumzmhm  19874  gsumzoppg  19881  dprdf1o  19971  imasrng  20093  imasring  20246  gsumfsum  21358  zncyg  21465  znf1o  21468  znleval  21471  znunit  21480  cygznlem2a  21484  indlcim  21756  cmpfi  23302  cnconn  23316  1stcfb  23339  qtopval2  23590  basqtop  23605  tgqtop  23606  imastopn  23614  hmeontr  23663  hmeoqtop  23669  nrmhmph  23688  cmphaushmeo  23694  elfm3  23844  qustgpopn  24014  tsmsf1o  24039  imasf1oxmet  24270  imasf1omet  24271  imasf1oxms  24384  cnheiborlem  24860  ovolctb  25398  dyadmbl  25508  dvcnvrelem2  25930  dvcnvre  25931  efifo  26463  circgrp  26468  circsubm  26469  logrn  26474  dvrelog  26553  efopnlem2  26573  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  bdayimaon  27612  noetasuplem4  27655  noetainflem4  27659  bdayrn  27694  noeta2  27703  negsunif  27968  negsbdaylem  27969  zssno  28276  f1otrg  28805  axcontlem10  28907  isgrpo  30433  isgrpoi  30434  pjrn  31643  padct  32650  cycpmconjvlem  33105  cycpmconjslem2  33119  imaslmod  33331  qusdimsum  33631  sigapildsys  34159  carsgclctunlem3  34318  ballotlemro  34521  erdsze2lem1  35197  cnpconn  35224  poimirlem15  37636  mblfinlem2  37659  volsupnfl  37666  ismtyres  37809  rngopidOLD  37854  opidon2OLD  37855  rngmgmbs4  37932  isgrpda  37956  mapdrn  41650  ricdrng1  42523  dnnumch2  43041  lnmlmic  43084  pwslnmlem1  43088  pwslnmlem2  43089  ntrneifv2  44076  ssnnf1octb  45195  stoweidlem27  46032  fourierdlem51  46162  fourierdlem102  46213  fourierdlem114  46225  sge0fodjrnlem  46421  nnfoctbdjlem  46460  nnfoctbdj  46461  3f1oss1  47080  fonex  48859  tposres3  48873