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

Theorem frel 5963
 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 5958 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnrel 5903 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴𝐵 → Rel 𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Rel wrel 5043   Fn wfn 5799  ⟶wf 5800 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 196  df-an 385  df-fun 5806  df-fn 5807  df-f 5808 This theorem is referenced by:  fssxp  5973  foconst  6039  fsn  6308  fnwelem  7179  mapsn  7785  axdc3lem4  9158  imasless  16023  gimcnv  17532  gsumval3  18131  lmimcnv  18888  mattpostpos  20079  hmeocnv  21375  metn0  21975  rlimcnp2  24493  wlkn0  26055  usgravd00  26446  mbfresfi  32626  seff  37530  fresin2  38347  mapsnd  38383  freld  38420  cncfuni  38772  fourierdlem48  39047  fourierdlem49  39048  fourierdlem113  39112  sge0cl  39274  1wlkn0  40825
 Copyright terms: Public domain W3C validator