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

Theorem frel 6492
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 6487 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnrel 6424 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5524   Fn wfn 6319  wf 6320
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 210  df-an 400  df-fun 6326  df-fn 6327  df-f 6328
This theorem is referenced by:  fssxp  6508  fimadmfoALT  6576  foconst  6578  fsn  6874  fnwelem  7808  mapsnd  8433  axdc3lem4  9864  imasless  16805  gimcnv  18399  gsumval3  19020  lmimcnv  19832  mattpostpos  21059  hmeocnv  22367  metn0  22967  rlimcnp2  25552  wlkn0  27410  tocyccntz  30836  mbfresfi  35103  seff  41011  fresin2  41794  freld  41857  cncfuni  42526  fourierdlem48  42794  fourierdlem49  42795  fourierdlem113  42859  sge0cl  43018
  Copyright terms: Public domain W3C validator