Theorem forn 6799

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5664   Fn wfn 6535  –onto→wfo 6538

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 6546

This theorem is used by:  dffo2  6800  foima  6801  fodmrnu  6804  focnvimacdmdm  6808  focofo  6809  foco  6810  f1imacnv  6841  foimacnv  6842  foun  6843  resdif  6846  fococnv2  6851  foelcdmi  6946  f1ounsn  7279  cbvfo  7296  f1ocoima  7310  isoini  7345  isofrlem  7347  isoselem  7348  canth  7373  f1opw2  7675  focdmex  7959  wemoiso2  7977  curry1  8105  curry2  8108  mapfoss  8855  bren  8959  en1  9027  fopwdom  9080  domss2  9131  mapen  9136  ssenen  9146  ssfiALT  9165  phplem2  9196  php3  9200  fodomfib  9295  f1opwfi  9320  ordiso2  9484  ordtypelem10  9496  oismo  9509  brwdom  9536  brwdom2  9542  wdomtr  9544  unxpwdom2  9557  wemapwe  9673  infxpenc2lem1  10019  fseqen  10027  fodomfi2  10060  infpwfien  10062  infmap2  10216  ackbij2  10241  infpssr  10307  fodomb  10525  fpwwe2lem5  10635  fpwwe2lem8  10638  tskuni  10783  gruen  10812  supcvg  15933  ruclem13  16320  unbenlem  16990  imasval  17587  imasaddfnlem  17604  imasvscafn  17613  imasless  17616  xpsfrn  17644  fulloppc  18003  mgmidprnd  18761  imasmnd2  18869  resgrpplusfrn  19061  imasgrp2  19165  oppglsm  19756  efgrelexlemb  19864  gsumzres  20023  gsumzcl2  20024  gsumzf1o  20026  gsumzaddlem  20035  gsumconst  20048  gsumzmhm  20051  gsumzoppg  20058  dprdf1o  20148  imasrng  20299  imasring  20458  gsumfsum  21634  zncyg  21748  znf1o  21751  znleval  21754  znunit  21763  cygznlem2a  21767  indlcim  22040  cmpfi  23615  cnconn  23629  1stcfb  23652  qtopval2  23904  basqtop  23919  tgqtop  23920  imastopn  23928  hmeontr  23977  hmeoqtop  23983  nrmhmph  24002  cmphaushmeo  24008  elfm3  24158  qustgpopn  24328  tsmsf1o  24353  imasf1oxmet  24583  imasf1omet  24584  imasf1oxms  24697  cnheiborlem  25164  ovolctb  25700  dyadmbl  25810  dvcnvrelem2  26228  dvcnvre  26229  efifo  26763  circgrp  26768  circsubm  26769  logrn  26774  dvrelog  26853  efopnlem2  26873  fsumdvdsmul  27410  bdayimaon  27908  noetasuplem4  27951  noetainflem4  27955  bdayrn  27995  noeta2  28005  negsunif  28299  negbdaylem  28300  zssno  28625  f1otrg  29275  axcontlem10  29378  isgrpo  30920  isgrpoi  30921  pjrn  32130  padct  33133  cycpmconjvlem  33525  cycpmconjslem2  33539  imaslmod  33737  esplysply  34025  qusdimsum  34082  sigapildsys  34617  carsgclctunlem3  34775  ballotlemro  34978  onvfowev  35657  erdsze2lem1  35732  cnpconn  35759  poimirlem15  38343  mblfinlem2  38366  volsupnfl  38373  ismtyres  38517  rngopidOLD  38562  opidon2OLD  38563  rngmgmbs4  38640  isgrpda  38664  mapdrn  42481  ricdrng1  43354  dnnumch2  43830  lnmlmic  43873  pwslnmlem1  43877  pwslnmlem2  43878  ntrneifv2  44864  ssnnf1octb  45970  stoweidlem27  46799  fourierdlem51  46929  fourierdlem102  46980  fourierdlem114  46992  sge0fodjrnlem  47188  nnfoctbdjlem  47227  nnfoctbdj  47228  3f1oss1  47870  fonex  49702  tposres3  49716