Theorem frel 6711

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

Syntax hints:   → wi 4  Rel wrel 5659   Fn wfn 6526  ⟶wf 6527

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 6533  df-fn 6534  df-f 6535

This theorem is referenced by:  freld  6712  fssxp  6733  fimadmfoALT  6801  foconst  6805  fsn  7125  fnwelem  8130  mapsnd  8900  axdc3lem4  10467  imasless  17554  gimcnv  19250  gsumval3  19888  rngimcnv  20416  lmimcnv  21025  mattpostpos  22392  hmeocnv  23700  metn0  24299  rlimcnp2  26928  wlkn0  29601  cyclnumvtx  29782  tocyccntz  33155  mbfresfi  37690  rimcnv  42540  seff  44333  fresin2  45196  cncfuni  45915  fourierdlem48  46183  fourierdlem49  46184  fourierdlem113  46248  sge0cl  46410