Theorem frel 6752

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

Syntax hints:   → wi 4  Rel wrel 5705   Fn wfn 6568  ⟶wf 6569

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 6575  df-fn 6576  df-f 6577

This theorem is referenced by:  freld  6753  fssxp  6775  fimadmfoALT  6845  foconst  6849  fsn  7169  fnwelem  8172  mapsnd  8944  axdc3lem4  10522  imasless  17600  gimcnv  19307  gsumval3  19949  rngimcnv  20482  lmimcnv  21089  mattpostpos  22481  hmeocnv  23791  metn0  24391  rlimcnp2  27027  wlkn0  29657  tocyccntz  33137  mbfresfi  37626  rimcnv  42472  seff  44278  fresin2  45079  cncfuni  45807  fourierdlem48  46075  fourierdlem49  46076  fourierdlem113  46140  sge0cl  46302