Theorem frel 6605

Description: A mapping is a relation. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
frel	⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹)

Proof of Theorem frel

Step	Hyp	Ref	Expression
1		ffn 6600	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnrel 6535	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹)

Syntax hints:   → wi 4  Rel wrel 5594   Fn wfn 6428  ⟶wf 6429

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 206  df-an 397  df-fun 6435  df-fn 6436  df-f 6437

This theorem is referenced by:  freld  6606  fssxp  6628  fimadmfoALT  6699  foconst  6703  fsn  7007  fnwelem  7972  mapsnd  8674  axdc3lem4  10209  imasless  17251  gimcnv  18883  gsumval3  19508  lmimcnv  20329  mattpostpos  21603  hmeocnv  22913  metn0  23513  rlimcnp2  26116  wlkn0  27988  tocyccntz  31411  mbfresfi  35823  seff  41927  fresin2  42708  cncfuni  43427  fourierdlem48  43695  fourierdlem49  43696  fourierdlem113  43760  sge0cl  43919