Theorem frel 6656

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

Syntax hints:   → wi 4  Rel wrel 5621   Fn wfn 6476  ⟶wf 6477

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 6483  df-fn 6484  df-f 6485

This theorem is referenced by:  freld  6657  fssxp  6678  fimadmfoALT  6746  foconst  6750  fsn  7068  fnwelem  8061  mapsnd  8810  axdc3lem4  10344  imasless  17444  gimcnv  19180  gsumval3  19820  rngimcnv  20375  lmimcnv  21002  mattpostpos  22370  hmeocnv  23678  metn0  24276  rlimcnp2  26904  wlkn0  29600  cyclnumvtx  29779  tocyccntz  33111  mbfresfi  37712  rimcnv  42556  seff  44348  fresin2  45215  cncfuni  45930  fourierdlem48  46198  fourierdlem49  46199  fourierdlem113  46263  sge0cl  46425