Theorem forn 6804

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ran crn 5652   Fn wfn 6538  –onto→wfo 6541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fo 6549

This theorem is used by:  dffo2  6805  foima  6806  fodmrnu  6809  focnvimacdmdm  6813  focofo  6814  foco  6815  f1imacnv  6846  foimacnv  6847  foun  6848  resdif  6851  fococnv2  6856  foelcdmi  6951  f1ounsn  7284  cbvfo  7301  f1ocoima  7315  isoini  7350  isofrlem  7352  isoselem  7353  canth  7378  f1opw2  7680  focdmex  7972  wemoiso2  7990  curry1  8121  curry2  8124  mapfoss  8881  bren  8990  en1  9058  fopwdom  9111  domss2  9162  mapen  9167  ssenen  9177  ssfiALT  9196  phplem2  9227  php3  9231  fodomfib  9327  f1opwfi  9352  ordiso2  9516  ordtypelem10  9528  oismo  9541  brwdom  9568  brwdom2  9574  wdomtr  9576  unxpwdom2  9589  wemapwe  9705  infxpenc2lem1  10105  fseqen  10113  fodomfi2  10146  infpwfien  10148  infmap2  10302  ackbij2  10327  infpssr  10393  fodomb  10612  fpwwe2lem5  10727  fpwwe2lem8  10730  tskuni  10875  gruen  10904  supcvg  16034  ruclem13  16419  unbenlem  17095  imasval  17692  imasaddfnlem  17709  imasvscafn  17718  imasless  17721  xpsfrn  17749  fulloppc  18108  mgmidprnd  18867  imasmgm2  18872  imasmnd2  18977  resgrpplusfrn  19170  imasgrp2  19274  oppglsm  19865  efgrelexlemb  19973  gsumzres  20132  gsumzcl2  20133  gsumzf1o  20135  gsumzaddlem  20144  gsumconst  20157  gsumzmhm  20160  gsumzoppg  20167  dprdf1o  20257  imasrng  20408  imasring  20569  gsumfsum  21749  zncyg  21863  znf1o  21866  znleval  21869  znunit  21878  cygznlem2a  21882  indlcim  22155  cmpfi  23735  cnconn  23749  1stcfb  23772  qtopval2  24024  basqtop  24039  tgqtop  24040  imastopn  24048  hmeontr  24097  hmeoqtop  24103  nrmhmph  24122  cmphaushmeo  24128  elfm3  24278  qustgpopn  24448  tsmsf1o  24473  imasf1oxmet  24703  imasf1omet  24704  imasf1oxms  24817  cnheiborlem  25284  ovolctb  25820  dyadmbl  25930  dvcnvrelem2  26347  dvcnvre  26348  efifo  26884  circgrp  26889  circsubm  26890  logrn  26895  dvrelog  26974  efopnlem2  26994  fsumdvdsmul  27531  bdayimaon  28059  noetasuplem4  28102  noetainflem4  28106  bdayrn  28146  negsunif  28450  negbdaylem  28451  zssno  28776  f1otrg  29457  axcontlem10  29560  isgrpo  31108  isgrpoi  31109  pjrn  32318  padct  33361  cycpmconjvlem  33752  cycpmconjslem2  33766  imaslmod  33964  esplysply  34253  qusdimsum  34310  sigapildsys  34845  carsgclctunlem3  35002  ballotlemro  35205  prconf1acwevd  35971  onvfowev  35973  erdsze2lem1  36058  cnpconn  36085  poimirlem15  38662  mblfinlem2  38685  volsupnfl  38692  ismtyres  38851  rngopidOLD  38896  opidon2OLD  38897  rngmgmbs4  38974  isgrpda  38998  mapdrn  42815  ricdrng1  43701  dnnumch2  44161  lnmlmic  44199  pwslnmlem1  44203  pwslnmlem2  44204  ntrneifv2  45189  ssnnf1octb  46317  stoweidlem27  47145  fourierdlem51  47275  fourierdlem102  47326  fourierdlem114  47338  sge0fodjrnlem  47534  nnfoctbdjlem  47573  nnfoctbdj  47574  3f1oss1  48253  fonex  50086  tposres3  50102