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

Theorem frel 5408
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 5405 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnrel 5358 . 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 4710    Fn wfn 5266   -->wf 5267
This theorem is referenced by:  fssxp  5416  foconst  5478  fsn  5712  fnwelem  6246  mapsn  6825  axdc3lem4  8095  imasless  13458  gimcnv  14747  gsumval3  15207  lmimcnv  15836  hmeocnv  17469  metn0  17940  rlimcnp2  20277  seff  27641
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 5273  df-fn 5274  df-f 5275
  Copyright terms: Public domain W3C validator