Theorem frel 6661

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

Syntax hints:   → wi 4  Rel wrel 5624   Fn wfn 6481  ⟶wf 6482

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 6488  df-fn 6489  df-f 6490

This theorem is referenced by:  freld  6662  fssxp  6683  fimadmfoALT  6751  foconst  6755  fsn  7074  fnwelem  8067  mapsnd  8816  axdc3lem4  10351  imasless  17446  gimcnv  19181  gsumval3  19821  rngimcnv  20376  lmimcnv  21003  mattpostpos  22370  hmeocnv  23678  metn0  24276  rlimcnp2  26904  wlkn0  29601  cyclnumvtx  29780  tocyccntz  33120  mbfresfi  37727  rimcnv  42636  seff  44427  fresin2  45294  cncfuni  46009  fourierdlem48  46277  fourierdlem49  46278  fourierdlem113  46342  sge0cl  46504