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

Theorem frel 5665
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 5662 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnrel 5612 . 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 4948    Fn wfn 5516   -->wf 5517
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 371  df-fun 5523  df-fn 5524  df-f 5525
This theorem is referenced by:  fssxp  5673  foconst  5734  fsn  5985  fnwelem  6792  mapsn  7359  axdc3lem4  8728  imasless  14592  gimcnv  15909  gsumval3OLD  16498  gsumval3  16501  lmimcnv  17266  mattpostpos  18460  hmeocnv  19462  metn0  20062  rlimcnp2  22488  mbfresfi  28581  seff  29738  wlkn0  30422  usgravd00  30681
  Copyright terms: Public domain W3C validator