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

Theorem frel 6349
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 6344 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnrel 6287 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5412   Fn wfn 6183  wf 6184
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 199  df-an 388  df-fun 6190  df-fn 6191  df-f 6192
This theorem is referenced by:  fssxp  6363  fimadmfoALT  6430  foconst  6432  fsn  6720  fnwelem  7630  mapsnd  8248  axdc3lem4  9673  imasless  16669  gimcnv  18178  gsumval3  18781  lmimcnv  19561  mattpostpos  20767  hmeocnv  22074  metn0  22673  rlimcnp2  25246  wlkn0  27105  mbfresfi  34376  seff  40054  fresin2  40850  freld  40917  cncfuni  41597  fourierdlem48  41868  fourierdlem49  41869  fourierdlem113  41933  sge0cl  42092
  Copyright terms: Public domain W3C validator