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

Theorem dffn4 5457
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 2283 . . 3  |-  ran  F  =  ran  F
21biantru 491 . 2  |-  ( F  Fn  A  <->  ( F  Fn  A  /\  ran  F  =  ran  F ) )
3 df-fo 5261 . 2  |-  ( F : A -onto-> ran  F  <->  ( F  Fn  A  /\  ran  F  =  ran  F
) )
42, 3bitr4i 243 1  |-  ( F  Fn  A  <->  F : A -onto-> ran  F )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    = wceq 1623   ran crn 4690    Fn wfn 5250   -onto->wfo 5253
This theorem is referenced by:  funforn  5458  ffoss  5505  tposf2  6258  mapsn  6809  fidomdm  7138  pwfilem  7150  indexfi  7163  intrnfi  7170  fifo  7185  ixpiunwdom  7305  infpwfien  7689  infmap2  7844  cfflb  7885  cfslb2n  7894  ttukeylem6  8141  fnrndomg  8160  rankcf  8399  tskuni  8405  tskurn  8411  fseqsupcl  11039  vdwlem6  13033  0ram2  13068  0ramcl  13070  divslem  13445  gsumval3  15191  gsumzoppg  15216  mplsubrglem  16183  rncmp  17123  cmpsub  17127  tgcmp  17128  hauscmplem  17133  concn  17152  2ndcctbss  17181  2ndcomap  17184  2ndcsep  17185  ptcnplem  17315  txtube  17334  txcmplem1  17335  tx1stc  17344  tx2ndc  17345  qtopid  17396  qtopcmplem  17398  qtopkgen  17401  kqtopon  17418  kqopn  17425  kqcld  17426  qtopf1  17507  rnelfm  17648  fmfnfmlem2  17650  fmfnfm  17653  alexsubALT  17745  ptcmplem2  17747  tmdgsum2  17779  tsmsxplem1  17835  met1stc  18067  met2ndci  18068  uniiccdif  18933  dyadmbl  18955  mbfimaopnlem  19010  i1fadd  19050  i1fmul  19051  itg1addlem4  19054  i1fmulc  19058  mbfi1fseqlem4  19073  limciun  19244  aannenlem3  19710  logccv  20010  dmct  23342  comppfsc  26307  istotbnd3  26495  sstotbnd  26499  prdsbnd  26517  cntotbnd  26520  heiborlem1  26535  heibor  26545  dihintcl  31534
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276  df-fo 5261
  Copyright terms: Public domain W3C validator