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

Theorem frel 6741
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 6736 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnrel 6670 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5690   Fn wfn 6556  wf 6557
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 207  df-an 396  df-fun 6563  df-fn 6564  df-f 6565
This theorem is referenced by:  freld  6742  fssxp  6763  fimadmfoALT  6831  foconst  6835  fsn  7155  fnwelem  8156  mapsnd  8926  axdc3lem4  10493  imasless  17585  gimcnv  19285  gsumval3  19925  rngimcnv  20456  lmimcnv  21066  mattpostpos  22460  hmeocnv  23770  metn0  24370  rlimcnp2  27009  wlkn0  29639  cyclnumvtx  29820  tocyccntz  33164  mbfresfi  37673  rimcnv  42527  seff  44328  fresin2  45177  cncfuni  45901  fourierdlem48  46169  fourierdlem49  46170  fourierdlem113  46234  sge0cl  46396
  Copyright terms: Public domain W3C validator