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

Theorem frel 6728
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 6723 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnrel 6657 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5683   Fn wfn 6544  wf 6545
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 395  df-fun 6551  df-fn 6552  df-f 6553
This theorem is referenced by:  freld  6729  fssxp  6751  fimadmfoALT  6821  foconst  6825  fsn  7144  fnwelem  8136  mapsnd  8905  axdc3lem4  10478  imasless  17525  gimcnv  19230  gsumval3  19874  rngimcnv  20407  lmimcnv  20964  mattpostpos  22400  hmeocnv  23710  metn0  24310  rlimcnp2  26943  wlkn0  29507  tocyccntz  32957  mbfresfi  37270  rimcnv  41892  seff  43888  fresin2  44684  cncfuni  45412  fourierdlem48  45680  fourierdlem49  45681  fourierdlem113  45745  sge0cl  45907
  Copyright terms: Public domain W3C validator