Theorem frel 6728

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

Syntax hints:   → wi 4  Rel wrel 5683   Fn wfn 6544  ⟶wf 6545

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 206  df-an 395  df-fun 6551  df-fn 6552  df-f 6553

This theorem is referenced by:  freld  6729  fssxp  6751  fimadmfoALT  6821  foconst  6825  fsn  7144  fnwelem  8136  mapsnd  8905  axdc3lem4  10478  imasless  17525  gimcnv  19230  gsumval3  19874  rngimcnv  20407  lmimcnv  20964  mattpostpos  22400  hmeocnv  23710  metn0  24310  rlimcnp2  26943  wlkn0  29507  tocyccntz  32957  mbfresfi  37270  rimcnv  41892  seff  43888  fresin2  44684  cncfuni  45412  fourierdlem48  45680  fourierdlem49  45681  fourierdlem113  45745  sge0cl  45907