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

Theorem frel 6088
 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 6083 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnrel 6027 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴𝐵 → Rel 𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Rel wrel 5148   Fn wfn 5921  ⟶wf 5922 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 197  df-an 385  df-fun 5928  df-fn 5929  df-f 5930 This theorem is referenced by:  fssxp  6098  foconst  6164  fsn  6442  fnwelem  7337  mapsn  7941  axdc3lem4  9313  imasless  16247  gimcnv  17756  gsumval3  18354  lmimcnv  19115  mattpostpos  20308  hmeocnv  21613  metn0  22212  rlimcnp2  24738  wlkn0  26572  mbfresfi  33586  seff  38825  fresin2  39666  mapsnd  39702  freld  39739  cncfuni  40417  fourierdlem48  40689  fourierdlem49  40690  fourierdlem113  40754  sge0cl  40916
 Copyright terms: Public domain W3C validator