Theorem frel 6707

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

This proof depends on syntax axioms:   → wi 4  Rel wrel 5656   Fn wfn 6526  ⟶wf 6527

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fun 6533  df-fn 6534  df-f 6535

This theorem is used by:  freld  6708  fssxp  6729  fimadmfoALT  6799  foconst  6803  fsn  7128  fnwelem  8132  mapsnd  8898  axdc3lem4  10512  imasless  17692  gimcnv  19461  gsumval3  20101  rngimcnv  20666  rimcnv  20697  lmimcnv  21322  mattpostpos  22749  hmeocnv  24061  metn0  24659  rlimcnp2  27276  wlkn0  30183  tocyccntz  33687  mbfresfi  38552  seff  45252  sge0cl  47335