Theorem frel 6088

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

Syntax hints:   → wi 4  Rel wrel 5148   Fn wfn 5921  ⟶wf 5922

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 197  df-an 385  df-fun 5928  df-fn 5929  df-f 5930

This theorem is referenced by:  fssxp  6098  foconst  6164  fsn  6442  fnwelem  7337  mapsn  7941  axdc3lem4  9313  imasless  16247  gimcnv  17756  gsumval3  18354  lmimcnv  19115  mattpostpos  20308  hmeocnv  21613  metn0  22212  rlimcnp2  24738  wlkn0  26572  mbfresfi  33586  seff  38825  fresin2  39666  mapsnd  39702  freld  39739  cncfuni  40417  fourierdlem48  40689  fourierdlem49  40690  fourierdlem113  40754  sge0cl  40916