Theorem forn 6614

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

Syntax hints:   → wi 4   = wceq 1543  ran crn 5537   Fn wfn 6353  –onto→wfo 6356

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 210  df-an 400  df-fo 6364

This theorem is referenced by:  dffo2  6615  foima  6616  fodmrnu  6619  focnvimacdmdm  6623  focofo  6624  foco  6625  f1imacnv  6655  foimacnv  6656  foun  6657  resdif  6659  fococnv2  6664  foelrni  6752  cbvfo  7077  isoini  7125  isofrlem  7127  isoselem  7128  canth  7145  f1opw2  7438  fornex  7707  wemoiso2  7725  curry1  7850  curry2  7853  mapfoss  8511  bren  8614  brenOLD  8615  en1  8676  en1OLD  8677  fopwdom  8731  domss2  8783  mapen  8788  ssenen  8798  phplem4  8806  php3  8810  ssfiOLD  8873  fodomfib  8928  f1opwfi  8958  ordiso2  9109  ordtypelem10  9121  oismo  9134  brwdom  9161  brwdom2  9167  wdomtr  9169  unxpwdom2  9182  wemapwe  9290  infxpenc2lem1  9598  fseqen  9606  fodomfi2  9639  infpwfien  9641  infmap2  9797  ackbij2  9822  infpssr  9887  fodomb  10105  fpwwe2lem5  10214  fpwwe2lem8  10217  tskuni  10362  gruen  10391  focdmex  13882  hashfacenOLD  13984  supcvg  15383  ruclem13  15766  unbenlem  16424  imasval  16970  imasaddfnlem  16987  imasvscafn  16996  imasless  16999  xpsfrn  17027  fulloppc  17383  imasmnd2  18164  resgrpplusfrn  18335  imasgrp2  18432  oppglsm  18985  efgrelexlemb  19094  gsumzres  19248  gsumzcl2  19249  gsumzf1o  19251  gsumzaddlem  19260  gsumconst  19273  gsumzmhm  19276  gsumzoppg  19283  dprdf1o  19373  imasring  19591  gsumfsum  20384  zncyg  20467  znf1o  20470  znleval  20473  znunit  20482  cygznlem2a  20486  indlcim  20756  cmpfi  22259  cnconn  22273  1stcfb  22296  qtopval2  22547  basqtop  22562  tgqtop  22563  imastopn  22571  hmeontr  22620  hmeoqtop  22626  nrmhmph  22645  cmphaushmeo  22651  elfm3  22801  qustgpopn  22971  tsmsf1o  22996  imasf1oxmet  23227  imasf1omet  23228  imasf1oxms  23341  cnheiborlem  23805  ovolctb  24341  dyadmbl  24451  dvcnvrelem2  24869  dvcnvre  24870  efifo  25390  circgrp  25395  circsubm  25396  logrn  25401  dvrelog  25479  efopnlem2  25499  fsumdvdsmul  26031  f1otrg  26916  axcontlem10  27018  isgrpo  28532  isgrpoi  28533  pjrn  29742  padct  30728  cycpmconjvlem  31081  cycpmconjslem2  31095  imaslmod  31221  qusdimsum  31377  sigapildsys  31796  carsgclctunlem3  31953  ballotlemro  32155  erdsze2lem1  32832  cnpconn  32859  bdayimaon  33582  noetasuplem4  33625  noetainflem4  33629  bdayrn  33656  noeta2  33665  poimirlem15  35478  mblfinlem2  35501  volsupnfl  35508  ismtyres  35652  rngopidOLD  35697  opidon2OLD  35698  rngmgmbs4  35775  isgrpda  35799  mapdrn  39349  dnnumch2  40514  lnmlmic  40557  pwslnmlem1  40561  pwslnmlem2  40562  ntrneifv2  41308  ssnnf1octb  42347  stoweidlem27  43186  fourierdlem51  43316  fourierdlem102  43367  fourierdlem114  43379  sge0fodjrnlem  43572  nnfoctbdjlem  43611  nnfoctbdj  43612