Theorem forn 6837

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

Syntax hints:   → wi 4   = wceq 1537  ran crn 5701   Fn wfn 6568  –onto→wfo 6571

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 207  df-an 396  df-fo 6579

This theorem is referenced by:  dffo2  6838  foima  6839  fodmrnu  6842  focnvimacdmdm  6846  focofo  6847  foco  6848  f1imacnv  6878  foimacnv  6879  foun  6880  resdif  6883  fococnv2  6888  foelcdmi  6983  cbvfo  7325  f1ocoima  7339  isoini  7374  isofrlem  7376  isoselem  7377  canth  7401  f1opw2  7705  focdmex  7996  wemoiso2  8015  curry1  8145  curry2  8148  mapfoss  8910  bren  9013  brenOLD  9014  en1  9086  en1OLD  9087  fopwdom  9146  domss2  9202  mapen  9207  ssenen  9217  ssfiALT  9241  phplem2  9271  php3  9275  phplem4OLD  9283  php3OLD  9287  fodomfib  9397  fodomfibOLD  9399  f1opwfi  9426  ordiso2  9584  ordtypelem10  9596  oismo  9609  brwdom  9636  brwdom2  9642  wdomtr  9644  unxpwdom2  9657  wemapwe  9766  infxpenc2lem1  10088  fseqen  10096  fodomfi2  10129  infpwfien  10131  infmap2  10286  ackbij2  10311  infpssr  10377  fodomb  10595  fpwwe2lem5  10704  fpwwe2lem8  10707  tskuni  10852  gruen  10881  supcvg  15904  ruclem13  16290  unbenlem  16955  imasval  17571  imasaddfnlem  17588  imasvscafn  17597  imasless  17600  xpsfrn  17628  fulloppc  17989  imasmnd2  18809  resgrpplusfrn  18990  imasgrp2  19095  oppglsm  19684  efgrelexlemb  19792  gsumzres  19951  gsumzcl2  19952  gsumzf1o  19954  gsumzaddlem  19963  gsumconst  19976  gsumzmhm  19979  gsumzoppg  19986  dprdf1o  20076  imasrng  20204  imasring  20353  gsumfsum  21475  zncyg  21590  znf1o  21593  znleval  21596  znunit  21605  cygznlem2a  21609  indlcim  21883  cmpfi  23437  cnconn  23451  1stcfb  23474  qtopval2  23725  basqtop  23740  tgqtop  23741  imastopn  23749  hmeontr  23798  hmeoqtop  23804  nrmhmph  23823  cmphaushmeo  23829  elfm3  23979  qustgpopn  24149  tsmsf1o  24174  imasf1oxmet  24406  imasf1omet  24407  imasf1oxms  24523  cnheiborlem  25005  ovolctb  25544  dyadmbl  25654  dvcnvrelem2  26077  dvcnvre  26078  efifo  26607  circgrp  26612  circsubm  26613  logrn  26618  dvrelog  26697  efopnlem2  26717  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  bdayimaon  27756  noetasuplem4  27799  noetainflem4  27803  bdayrn  27838  noeta2  27847  negsunif  28105  negsbdaylem  28106  zssno  28385  f1otrg  28897  axcontlem10  29006  isgrpo  30529  isgrpoi  30530  pjrn  31739  padct  32733  cycpmconjvlem  33134  cycpmconjslem2  33148  imaslmod  33346  qusdimsum  33641  sigapildsys  34126  carsgclctunlem3  34285  ballotlemro  34487  erdsze2lem1  35171  cnpconn  35198  poimirlem15  37595  mblfinlem2  37618  volsupnfl  37625  ismtyres  37768  rngopidOLD  37813  opidon2OLD  37814  rngmgmbs4  37891  isgrpda  37915  mapdrn  41606  ricdrng1  42483  dnnumch2  43002  lnmlmic  43045  pwslnmlem1  43049  pwslnmlem2  43050  ntrneifv2  44042  ssnnf1octb  45101  stoweidlem27  45948  fourierdlem51  46078  fourierdlem102  46129  fourierdlem114  46141  sge0fodjrnlem  46337  nnfoctbdjlem  46376  nnfoctbdj  46377  3f1oss1  46990  uspgrimprop  47757