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 5630   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 208  df-an 397  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  freld  6668  fssxp  6689  fimadmfoALT  6757  foconst  6761  fsn  7084  fnwelem  8078  mapsnd  8831  axdc3lem4  10373  imasless  17502  gimcnv  19240  gsumval3  19880  rngimcnv  20434  rimcnv  20463  lmimcnv  21064  mattpostpos  22444  hmeocnv  23752  metn0  24350  rlimcnp2  26955  wlkn0  29714  cyclnumvtx  29893  tocyccntz  33232  mbfresfi  38040  seff  44760  fresin2  45626  cncfuni  46336  fourierdlem48  46604  fourierdlem49  46605  fourierdlem113  46669  sge0cl  46831