Theorem frel 6667

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

Syntax hints:   → wi 4  Rel wrel 5629   Fn wfn 6487  ⟶wf 6488

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 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  freld  6668  fssxp  6689  fimadmfoALT  6757  foconst  6761  fsn  7082  fnwelem  8074  mapsnd  8827  axdc3lem4  10366  imasless  17495  gimcnv  19233  gsumval3  19873  rngimcnv  20427  lmimcnv  21054  mattpostpos  22429  hmeocnv  23737  metn0  24335  rlimcnp2  26943  wlkn0  29704  cyclnumvtx  29883  tocyccntz  33220  mbfresfi  38001  rimcnv  42976  seff  44754  fresin2  45620  cncfuni  46332  fourierdlem48  46600  fourierdlem49  46601  fourierdlem113  46665  sge0cl  46827