MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dffn4 Unicode version

Theorem dffn4 5618
Description: A function maps onto its range. (Contributed by NM, 10-May-1998.)
Assertion
Ref Expression
dffn4  |-  ( F  Fn  A  <->  F : A -onto-> ran  F )

Proof of Theorem dffn4
StepHypRef Expression
1 eqid 2404 . . 3  |-  ran  F  =  ran  F
21biantru 492 . 2  |-  ( F  Fn  A  <->  ( F  Fn  A  /\  ran  F  =  ran  F ) )
3 df-fo 5419 . 2  |-  ( F : A -onto-> ran  F  <->  ( F  Fn  A  /\  ran  F  =  ran  F
) )
42, 3bitr4i 244 1  |-  ( F  Fn  A  <->  F : A -onto-> ran  F )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    = wceq 1649   ran crn 4838    Fn wfn 5408   -onto->wfo 5411
This theorem is referenced by:  funforn  5619  ffoss  5666  tposf2  6462  mapsn  7014  fidomdm  7347  pwfilem  7359  indexfi  7372  intrnfi  7379  fifo  7395  ixpiunwdom  7515  infpwfien  7899  infmap2  8054  cfflb  8095  cfslb2n  8104  ttukeylem6  8350  fnrndomg  8369  rankcf  8608  tskuni  8614  tskurn  8620  fseqsupcl  11271  vdwlem6  13309  0ram2  13344  0ramcl  13346  divslem  13723  gsumval3  15469  gsumzoppg  15494  mplsubrglem  16457  rncmp  17413  cmpsub  17417  tgcmp  17418  hauscmplem  17423  concn  17442  2ndcctbss  17471  2ndcomap  17474  2ndcsep  17475  ptcnplem  17606  txtube  17625  txcmplem1  17626  tx1stc  17635  tx2ndc  17636  qtopid  17690  qtopcmplem  17692  qtopkgen  17695  kqtopon  17712  kqopn  17719  kqcld  17720  qtopf1  17801  rnelfm  17938  fmfnfmlem2  17940  fmfnfm  17943  alexsubALT  18035  ptcmplem2  18037  tmdgsum2  18079  tsmsxplem1  18135  met1stc  18504  met2ndci  18505  uniiccdif  19423  dyadmbl  19445  mbfimaopnlem  19500  i1fadd  19540  i1fmul  19541  itg1addlem4  19544  i1fmulc  19548  mbfi1fseqlem4  19563  limciun  19734  aannenlem3  20200  logccv  20507  dmct  24059  itg2addnclem2  26156  comppfsc  26277  istotbnd3  26370  sstotbnd  26374  prdsbnd  26392  cntotbnd  26395  heiborlem1  26410  heibor  26420  dihintcl  31827
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-cleq 2397  df-fo 5419
  Copyright terms: Public domain W3C validator