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

Theorem frel 6674
Description: A mapping is a relation. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
frel (𝐹:𝐴𝐵 → Rel 𝐹)

Proof of Theorem frel
StepHypRef Expression
1 ffn 6669 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnrel 6605 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5639   Fn wfn 6492  wf 6493
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 206  df-an 398  df-fun 6499  df-fn 6500  df-f 6501
This theorem is referenced by:  freld  6675  fssxp  6697  fimadmfoALT  6768  foconst  6772  fsn  7082  fnwelem  8064  mapsnd  8827  axdc3lem4  10394  imasless  17427  gimcnv  19062  gsumval3  19689  lmimcnv  20543  mattpostpos  21819  hmeocnv  23129  metn0  23729  rlimcnp2  26332  wlkn0  28611  tocyccntz  32042  mbfresfi  36170  rimcnv  40743  seff  42677  fresin2  43477  cncfuni  44213  fourierdlem48  44481  fourierdlem49  44482  fourierdlem113  44546  sge0cl  44708
  Copyright terms: Public domain W3C validator