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

Theorem frel 5739
Description: A mapping is a relation. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
frel

Proof of Theorem frel
StepHypRef Expression
1 ffn 5736 . 2
2 fnrel 5684 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  Relwrel 5009  Fnwfn 5588  -->wf 5589
This theorem is referenced by:  fssxp  5748  foconst  5811  fsn  6069  fnwelem  6915  mapsn  7480  axdc3lem4  8854  imasless  14937  gimcnv  16315  gsumval3OLD  16908  gsumval3  16911  lmimcnv  17713  mattpostpos  18956  hmeocnv  20263  metn0  20863  rlimcnp2  23296  wlkn0  24527  usgravd00  24919  mbfresfi  30061  seff  31189  fresin2  31448  cncfuni  31689  fourierdlem48  31937  fourierdlem49  31938  fourierdlem113  32002
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 5595  df-fn 5596  df-f 5597
  Copyright terms: Public domain W3C validator