Theorem forn 6796

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

Syntax hints:   → wi 4   = wceq 1567  ran crn 5663   Fn wfn 6532  –onto→wfo 6535

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 401  df-fo 6543

This theorem is referenced by:  dffo2  6797  foima  6798  fodmrnu  6801  focnvimacdmdm  6805  focofo  6806  foco  6807  f1imacnv  6838  foimacnv  6839  foun  6840  resdif  6843  fococnv2  6848  foelcdmi  6943  f1ounsn  7271  cbvfo  7288  f1ocoima  7302  isoini  7337  isofrlem  7339  isoselem  7340  canth  7365  f1opw2  7666  focdmex  7952  wemoiso2  7970  curry1  8098  curry2  8101  mapfoss  8848  bren  8952  en1  9020  fopwdom  9072  domss2  9123  mapen  9128  ssenen  9138  ssfiALT  9157  phplem2  9188  php3  9192  fodomfib  9287  f1opwfi  9312  ordiso2  9476  ordtypelem10  9488  oismo  9501  brwdom  9528  brwdom2  9534  wdomtr  9536  unxpwdom2  9549  wemapwe  9665  infxpenc2lem1  10002  fseqen  10010  fodomfi2  10043  infpwfien  10045  infmap2  10199  ackbij2  10224  infpssr  10291  fodomb  10509  fpwwe2lem5  10619  fpwwe2lem8  10622  tskuni  10767  gruen  10796  supcvg  15909  ruclem13  16297  unbenlem  16967  imasval  17564  imasaddfnlem  17581  imasvscafn  17590  imasless  17593  xpsfrn  17621  fulloppc  17980  imasmnd2  18831  resgrpplusfrn  19016  imasgrp2  19120  oppglsm  19711  efgrelexlemb  19819  gsumzres  19978  gsumzcl2  19979  gsumzf1o  19981  gsumzaddlem  19990  gsumconst  20003  gsumzmhm  20006  gsumzoppg  20013  dprdf1o  20103  imasrng  20254  imasring  20411  gsumfsum  21552  zncyg  21666  znf1o  21669  znleval  21672  znunit  21681  cygznlem2a  21685  indlcim  21958  cmpfi  23533  cnconn  23547  1stcfb  23570  qtopval2  23821  basqtop  23836  tgqtop  23837  imastopn  23845  hmeontr  23894  hmeoqtop  23900  nrmhmph  23919  cmphaushmeo  23925  elfm3  24075  qustgpopn  24245  tsmsf1o  24270  imasf1oxmet  24500  imasf1omet  24501  imasf1oxms  24614  cnheiborlem  25081  ovolctb  25617  dyadmbl  25727  dvcnvrelem2  26145  dvcnvre  26146  efifo  26677  circgrp  26682  circsubm  26683  logrn  26688  dvrelog  26767  efopnlem2  26787  fsumdvdsmul  27324  bdayimaon  27822  noetasuplem4  27865  noetainflem4  27869  bdayrn  27909  noeta2  27919  negsunif  28213  negbdaylem  28214  zssno  28539  f1otrg  29160  axcontlem10  29263  isgrpo  30789  isgrpoi  30790  pjrn  31999  padct  33003  cycpmconjvlem  33401  cycpmconjslem2  33415  imaslmod  33615  esplysply  33905  qusdimsum  33962  sigapildsys  34496  carsgclctunlem3  34654  ballotlemro  34857  onvfowev  35498  erdsze2lem1  35593  cnpconn  35620  poimirlem15  38173  mblfinlem2  38196  volsupnfl  38203  ismtyres  38346  rngopidOLD  38391  opidon2OLD  38392  rngmgmbs4  38469  isgrpda  38493  mapdrn  42312  ricdrng1  43187  dnnumch2  43663  lnmlmic  43706  pwslnmlem1  43710  pwslnmlem2  43711  ntrneifv2  44697  ssnnf1octb  45803  stoweidlem27  46632  fourierdlem51  46762  fourierdlem102  46813  fourierdlem114  46825  sge0fodjrnlem  47021  nnfoctbdjlem  47060  nnfoctbdj  47061  3f1oss1  47700  fonex  49529  tposres3  49543