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

Theorem frel 5392
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 5389 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnrel 5342 . 2  |-  ( F  Fn  A  ->  Rel  F )
31, 2syl 15 1  |-  ( F : A --> B  ->  Rel  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Rel wrel 4694    Fn wfn 5250   -->wf 5251
This theorem is referenced by:  fssxp  5400  foconst  5462  fsn  5696  fnwelem  6230  mapsn  6809  axdc3lem4  8079  imasless  13442  gimcnv  14731  gsumval3  15191  lmimcnv  15820  hmeocnv  17453  metn0  17924  rlimcnp2  20261  seff  27538
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-fun 5257  df-fn 5258  df-f 5259
  Copyright terms: Public domain W3C validator