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

Theorem dffn4 5688
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 2442 . . 3  |-  ran  F  =  ran  F
21biantru 493 . 2  |-  ( F  Fn  A  <->  ( F  Fn  A  /\  ran  F  =  ran  F ) )
3 df-fo 5489 . 2  |-  ( F : A -onto-> ran  F  <->  ( F  Fn  A  /\  ran  F  =  ran  F
) )
42, 3bitr4i 245 1  |-  ( F  Fn  A  <->  F : A -onto-> ran  F )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    = wceq 1653   ran crn 4908    Fn wfn 5478   -onto->wfo 5481
This theorem is referenced by:  funforn  5689  ffoss  5736  tposf2  6532  mapsn  7084  fidomdm  7417  pwfilem  7430  indexfi  7443  intrnfi  7450  fifo  7466  ixpiunwdom  7588  infpwfien  7974  infmap2  8129  cfflb  8170  cfslb2n  8179  ttukeylem6  8425  fnrndomg  8444  rankcf  8683  tskuni  8689  tskurn  8695  fseqsupcl  11347  vdwlem6  13385  0ram2  13420  0ramcl  13422  divslem  13799  gsumval3  15545  gsumzoppg  15570  mplsubrglem  16533  rncmp  17490  cmpsub  17494  tgcmp  17495  hauscmplem  17500  concn  17520  2ndcctbss  17549  2ndcomap  17552  2ndcsep  17553  ptcnplem  17684  txtube  17703  txcmplem1  17704  tx1stc  17713  tx2ndc  17714  qtopid  17768  qtopcmplem  17770  qtopkgen  17773  kqtopon  17790  kqopn  17797  kqcld  17798  qtopf1  17879  rnelfm  18016  fmfnfmlem2  18018  fmfnfm  18021  alexsubALT  18113  ptcmplem2  18115  tmdgsum2  18157  tsmsxplem1  18213  met1stc  18582  met2ndci  18583  uniiccdif  19501  dyadmbl  19523  mbfimaopnlem  19576  i1fadd  19616  i1fmul  19617  itg1addlem4  19620  i1fmulc  19624  mbfi1fseqlem4  19639  limciun  19812  aannenlem3  20278  logccv  20585  dmct  24137  itg2addnclem2  26295  comppfsc  26425  istotbnd3  26518  sstotbnd  26522  prdsbnd  26540  cntotbnd  26543  heiborlem1  26558  heibor  26568  dihintcl  32240
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-an 362  df-cleq 2435  df-fo 5489
  Copyright terms: Public domain W3C validator