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

Theorem frel 5596
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 5593 . 2  |-  ( F : A --> B  ->  F  Fn  A )
2 fnrel 5545 . 2  |-  ( F  Fn  A  ->  Rel  F )
31, 2syl 16 1  |-  ( F : A --> B  ->  Rel  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Rel wrel 4885    Fn wfn 5451   -->wf 5452
This theorem is referenced by:  fssxp  5604  foconst  5666  fsn  5908  fnwelem  6463  mapsn  7057  axdc3lem4  8335  imasless  13767  gimcnv  15056  gsumval3  15516  lmimcnv  16141  hmeocnv  17796  metn0  18392  rlimcnp2  20807  mbfresfi  26255  seff  27517  wlkn0  28320  usgravd00  28424
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 179  df-an 362  df-fun 5458  df-fn 5459  df-f 5460
  Copyright terms: Public domain W3C validator