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

Theorem forn 6568
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 6330 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
21simprbi 500 1 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  ran crn 5520   Fn wfn 6319  ontowfo 6322
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 400  df-fo 6330
This theorem is referenced by:  dffo2  6569  foima  6570  fodmrnu  6573  f1imacnv  6606  foimacnv  6607  foun  6608  resdif  6610  fococnv2  6615  foelrni  6702  cbvfo  7023  isoini  7070  isofrlem  7072  isoselem  7073  canth  7090  f1opw2  7380  fornex  7639  wemoiso2  7657  curry1  7782  curry2  7785  bren  8501  en1  8559  fopwdom  8608  domss2  8660  mapen  8665  ssenen  8675  phplem4  8683  php3  8687  ssfi  8722  fodomfib  8782  f1opwfi  8812  ordiso2  8963  ordtypelem10  8975  oismo  8988  brwdom  9015  brwdom2  9021  wdomtr  9023  unxpwdom2  9036  wemapwe  9144  infxpenc2lem1  9430  fseqen  9438  fodomfi2  9471  infpwfien  9473  infmap2  9629  ackbij2  9654  infpssr  9719  fodomb  9937  fpwwe2lem6  10046  fpwwe2lem9  10049  tskuni  10194  gruen  10223  focdmex  13707  hashfacen  13808  supcvg  15203  ruclem13  15587  unbenlem  16234  imasval  16776  imasaddfnlem  16793  imasvscafn  16802  imasless  16805  xpsfrn  16833  fulloppc  17184  imasmnd2  17940  resgrpplusfrn  18109  imasgrp2  18206  oppglsm  18759  efgrelexlemb  18868  gsumzres  19022  gsumzcl2  19023  gsumzf1o  19025  gsumzaddlem  19034  gsumconst  19047  gsumzmhm  19050  gsumzoppg  19057  dprdf1o  19147  imasring  19365  gsumfsum  20158  zncyg  20240  znf1o  20243  znleval  20246  znunit  20255  cygznlem2a  20259  indlcim  20529  cmpfi  22013  cnconn  22027  1stcfb  22050  qtopval2  22301  basqtop  22316  tgqtop  22317  imastopn  22325  hmeontr  22374  hmeoqtop  22380  nrmhmph  22399  cmphaushmeo  22405  elfm3  22555  qustgpopn  22725  tsmsf1o  22750  imasf1oxmet  22982  imasf1omet  22983  imasf1oxms  23096  cnheiborlem  23559  ovolctb  24094  dyadmbl  24204  dvcnvrelem2  24621  dvcnvre  24622  efifo  25139  circgrp  25144  circsubm  25145  logrn  25150  dvrelog  25228  efopnlem2  25248  fsumdvdsmul  25780  f1otrg  26665  axcontlem10  26767  isgrpo  28280  isgrpoi  28281  pjrn  29490  padct  30481  cycpmconjvlem  30833  cycpmconjslem2  30847  imaslmod  30973  qusdimsum  31112  sigapildsys  31531  carsgclctunlem3  31688  ballotlemro  31890  erdsze2lem1  32563  cnpconn  32590  bdayimaon  33310  nosupbday  33318  noetalem3  33332  noetalem4  33333  bdayrn  33358  poimirlem15  35072  mblfinlem2  35095  volsupnfl  35102  ismtyres  35246  rngopidOLD  35291  opidon2OLD  35292  rngmgmbs4  35369  isgrpda  35393  mapdrn  38945  dnnumch2  39987  lnmlmic  40030  pwslnmlem1  40034  pwslnmlem2  40035  ntrneifv2  40781  ssnnf1octb  41820  stoweidlem27  42667  fourierdlem51  42797  fourierdlem102  42848  fourierdlem114  42860  sge0fodjrnlem  43053  nnfoctbdjlem  43092  nnfoctbdj  43093
  Copyright terms: Public domain W3C validator