Theorem frel 6589

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 6584	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnrel 6519	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹)

Syntax hints:   → wi 4  Rel wrel 5585   Fn wfn 6413  ⟶wf 6414

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 396  df-fun 6420  df-fn 6421  df-f 6422

This theorem is referenced by:  freld  6590  fssxp  6612  fimadmfoALT  6683  foconst  6687  fsn  6989  fnwelem  7943  mapsnd  8632  axdc3lem4  10140  imasless  17168  gimcnv  18798  gsumval3  19423  lmimcnv  20244  mattpostpos  21511  hmeocnv  22821  metn0  23421  rlimcnp2  26021  wlkn0  27890  tocyccntz  31313  mbfresfi  35750  seff  41816  fresin2  42597  cncfuni  43317  fourierdlem48  43585  fourierdlem49  43586  fourierdlem113  43650  sge0cl  43809