MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  forn Structured version   Visualization version   GIF version

Theorem forn 6016
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
StepHypRef Expression
1 df-fo 5796 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
21simprbi 479 1 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  ran crn 5029   Fn wfn 5785  ontowfo 5788
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 196  df-an 385  df-fo 5796
This theorem is referenced by:  dffo2  6017  foima  6018  fodmrnu  6021  f1imacnv  6051  foimacnv  6052  foun  6053  resdif  6055  fococnv2  6060  foelrni  6139  cbvfo  6422  isoini  6466  isofrlem  6468  isoselem  6469  canth  6486  f1opw2  6764  fornex  7006  wemoiso2  7023  curry1  7134  curry2  7137  bren  7828  en1  7887  fopwdom  7931  domss2  7982  mapen  7987  ssenen  7997  phplem4  8005  php3  8009  ssfi  8043  fodomfib  8103  f1opwfi  8131  ordiso2  8281  ordtypelem10  8293  oismo  8306  brwdom  8333  brwdom2  8339  wdomtr  8341  unxpwdom2  8354  wemapwe  8455  infxpenc2lem1  8703  fseqen  8711  fodomfi2  8744  infpwfien  8746  infmap2  8901  ackbij2  8926  infpssr  8991  fodomb  9207  fpwwe2lem6  9314  fpwwe2lem9  9317  tskuni  9462  gruen  9491  focdmex  12956  hashfacen  13050  supcvg  14376  ruclem13  14759  unbenlem  15399  imasval  15943  imasaddfnlem  15960  imasvscafn  15969  imasless  15972  xpsfrn  16001  fulloppc  16354  imasmnd2  17099  resgrpplusfrn  17208  imasgrp2  17302  oppglsm  17829  efgrelexlemb  17935  gsumzres  18082  gsumzcl2  18083  gsumzf1o  18085  gsumzaddlem  18093  gsumconst  18106  gsumzmhm  18109  gsumzoppg  18116  dprdf1o  18203  imasring  18391  gsumfsum  19581  zncyg  19664  znf1o  19667  znleval  19670  znunit  19679  cygznlem2a  19683  indlcim  19946  cmpfi  20969  cnconn  20983  1stcfb  21006  qtopval2  21257  basqtop  21272  tgqtop  21273  imastopn  21281  hmeontr  21330  hmeoqtop  21336  nrmhmph  21355  cmphaushmeo  21361  elfm3  21512  qustgpopn  21681  tsmsf1o  21706  imasf1oxmet  21938  imasf1omet  21939  imasf1oxms  22052  cnheiborlem  22509  ovolctb  23010  dyadmbl  23119  dvcnvrelem2  23530  dvcnvre  23531  efifo  24042  circgrp  24047  circsubm  24048  logrn  24054  dvrelog  24128  efopnlem2  24148  fsumdvdsmul  24666  f1otrg  25497  axcontlem10  25599  eupares  26296  eupath2lem3  26300  isgrpo  26529  isgrpoi  26530  pjrn  27744  padct  28679  sigapildsys  29346  carsgclctunlem3  29503  ballotlemro  29705  erdsze2lem1  30233  cnpcon  30260  bdayrn  30870  poimirlem15  32388  mblfinlem2  32411  volsupnfl  32418  ismtyres  32571  rngopidOLD  32616  opidon2OLD  32617  rngmgmbs4  32694  isgrpda  32718  mapdrn  35750  dnnumch2  36427  lnmlmic  36470  pwslnmlem1  36474  pwslnmlem2  36475  ntrneifv2  37192  ssnnf1octb  38171  stoweidlem27  38714  fourierdlem51  38844  fourierdlem102  38895  fourierdlem114  38907  sge0fodjrnlem  39103  nnfoctbdjlem  39142  nnfoctbdj  39143
  Copyright terms: Public domain W3C validator