Theorem forn 6691

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

Syntax hints:   → wi 4   = wceq 1539  ran crn 5590   Fn wfn 6428  –onto→wfo 6431

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 206  df-an 397  df-fo 6439

This theorem is referenced by:  dffo2  6692  foima  6693  fodmrnu  6696  focnvimacdmdm  6700  focofo  6701  foco  6702  f1imacnv  6732  foimacnv  6733  foun  6734  resdif  6737  fococnv2  6742  foelrni  6831  cbvfo  7161  isoini  7209  isofrlem  7211  isoselem  7212  canth  7229  f1opw2  7524  fornex  7798  wemoiso2  7817  curry1  7944  curry2  7947  mapfoss  8640  bren  8743  brenOLD  8744  en1  8811  en1OLD  8812  fopwdom  8867  domss2  8923  mapen  8928  ssenen  8938  ssfiALT  8957  phplem2  8991  php3  8995  phplem4OLD  9003  php3OLD  9007  fodomfib  9093  f1opwfi  9123  ordiso2  9274  ordtypelem10  9286  oismo  9299  brwdom  9326  brwdom2  9332  wdomtr  9334  unxpwdom2  9347  wemapwe  9455  infxpenc2lem1  9775  fseqen  9783  fodomfi2  9816  infpwfien  9818  infmap2  9974  ackbij2  9999  infpssr  10064  fodomb  10282  fpwwe2lem5  10391  fpwwe2lem8  10394  tskuni  10539  gruen  10568  focdmex  14065  hashfacenOLD  14167  supcvg  15568  ruclem13  15951  unbenlem  16609  imasval  17222  imasaddfnlem  17239  imasvscafn  17248  imasless  17251  xpsfrn  17279  fulloppc  17638  imasmnd2  18422  resgrpplusfrn  18593  imasgrp2  18690  oppglsm  19247  efgrelexlemb  19356  gsumzres  19510  gsumzcl2  19511  gsumzf1o  19513  gsumzaddlem  19522  gsumconst  19535  gsumzmhm  19538  gsumzoppg  19545  dprdf1o  19635  imasring  19858  gsumfsum  20665  zncyg  20756  znf1o  20759  znleval  20762  znunit  20771  cygznlem2a  20775  indlcim  21047  cmpfi  22559  cnconn  22573  1stcfb  22596  qtopval2  22847  basqtop  22862  tgqtop  22863  imastopn  22871  hmeontr  22920  hmeoqtop  22926  nrmhmph  22945  cmphaushmeo  22951  elfm3  23101  qustgpopn  23271  tsmsf1o  23296  imasf1oxmet  23528  imasf1omet  23529  imasf1oxms  23645  cnheiborlem  24117  ovolctb  24654  dyadmbl  24764  dvcnvrelem2  25182  dvcnvre  25183  efifo  25703  circgrp  25708  circsubm  25709  logrn  25714  dvrelog  25792  efopnlem2  25812  fsumdvdsmul  26344  f1otrg  27232  axcontlem10  27341  isgrpo  28859  isgrpoi  28860  pjrn  30069  padct  31054  cycpmconjvlem  31408  cycpmconjslem2  31422  imaslmod  31553  qusdimsum  31709  sigapildsys  32130  carsgclctunlem3  32287  ballotlemro  32489  erdsze2lem1  33165  cnpconn  33192  bdayimaon  33896  noetasuplem4  33939  noetainflem4  33943  bdayrn  33970  noeta2  33979  poimirlem15  35792  mblfinlem2  35815  volsupnfl  35822  ismtyres  35966  rngopidOLD  36011  opidon2OLD  36012  rngmgmbs4  36089  isgrpda  36113  mapdrn  39663  dnnumch2  40870  lnmlmic  40913  pwslnmlem1  40917  pwslnmlem2  40918  ntrneifv2  41690  ssnnf1octb  42733  stoweidlem27  43568  fourierdlem51  43698  fourierdlem102  43749  fourierdlem114  43761  sge0fodjrnlem  43954  nnfoctbdjlem  43993  nnfoctbdj  43994