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