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

Theorem frel 5642
Description: A mapping is a relation. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
frel  |-  ( F : A --> B  ->  Rel  F )

Proof of Theorem frel
StepHypRef Expression
1 ffn 5639 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnrel 5587 . 2  |-  ( F  Fn  A  ->  Rel  F )
31, 2syl 16 1  |-  ( F : A --> B  ->  Rel  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   Rel wrel 4918    Fn wfn 5491   -->wf 5492
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 185  df-an 369  df-fun 5498  df-fn 5499  df-f 5500
This theorem is referenced by:  fssxp  5651  foconst  5714  fsn  5971  fnwelem  6814  mapsn  7379  axdc3lem4  8746  imasless  14947  gimcnv  16432  gsumval3OLD  17025  gsumval3  17028  lmimcnv  17826  mattpostpos  19041  hmeocnv  20348  metn0  20948  rlimcnp2  23413  wlkn0  24648  usgravd00  25040  mbfresfi  30226  seff  31357  fresin2  31615  cncfuni  31855  fourierdlem48  32103  fourierdlem49  32104  fourierdlem113  32168
  Copyright terms: Public domain W3C validator