Theorem frel 6513

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

Syntax hints:   → wi 4  Rel wrel 5554   Fn wfn 6344  ⟶wf 6345

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 209  df-an 399  df-fun 6351  df-fn 6352  df-f 6353

This theorem is referenced by:  fssxp  6528  fimadmfoALT  6595  foconst  6597  fsn  6891  fnwelem  7819  mapsnd  8444  axdc3lem4  9869  imasless  16807  gimcnv  18401  gsumval3  19021  lmimcnv  19833  mattpostpos  21057  hmeocnv  22364  metn0  22964  rlimcnp2  25538  wlkn0  27396  tocyccntz  30781  mbfresfi  34932  seff  40634  fresin2  41421  freld  41486  cncfuni  42162  fourierdlem48  42433  fourierdlem49  42434  fourierdlem113  42498  sge0cl  42657