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

Theorem dffn4 5563
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 2366 . . 3  |-  ran  F  =  ran  F
21biantru 491 . 2  |-  ( F  Fn  A  <->  ( F  Fn  A  /\  ran  F  =  ran  F ) )
3 df-fo 5364 . 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 1647   ran crn 4793    Fn wfn 5353   -onto->wfo 5356
This theorem is referenced by:  funforn  5564  ffoss  5611  tposf2  6400  mapsn  6952  fidomdm  7285  pwfilem  7297  indexfi  7310  intrnfi  7317  fifo  7332  ixpiunwdom  7452  infpwfien  7836  infmap2  7991  cfflb  8032  cfslb2n  8041  ttukeylem6  8288  fnrndomg  8307  rankcf  8546  tskuni  8552  tskurn  8558  fseqsupcl  11203  vdwlem6  13241  0ram2  13276  0ramcl  13278  divslem  13655  gsumval3  15401  gsumzoppg  15426  mplsubrglem  16393  rncmp  17340  cmpsub  17344  tgcmp  17345  hauscmplem  17350  concn  17369  2ndcctbss  17398  2ndcomap  17401  2ndcsep  17402  ptcnplem  17532  txtube  17551  txcmplem1  17552  tx1stc  17561  tx2ndc  17562  qtopid  17613  qtopcmplem  17615  qtopkgen  17618  kqtopon  17635  kqopn  17642  kqcld  17643  qtopf1  17724  rnelfm  17861  fmfnfmlem2  17863  fmfnfm  17866  alexsubALT  17958  ptcmplem2  17960  tmdgsum2  17992  tsmsxplem1  18048  met1stc  18280  met2ndci  18281  uniiccdif  19148  dyadmbl  19170  mbfimaopnlem  19225  i1fadd  19265  i1fmul  19266  itg1addlem4  19269  i1fmulc  19273  mbfi1fseqlem4  19288  limciun  19459  aannenlem3  19925  logccv  20232  dmct  23509  itg2addnclem2  25676  comppfsc  25814  istotbnd3  26001  sstotbnd  26005  prdsbnd  26023  cntotbnd  26026  heiborlem1  26041  heibor  26051  dihintcl  31605
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2359  df-fo 5364
  Copyright terms: Public domain W3C validator