Theorem frel 6715

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

This proof depends on syntax axioms:   → wi 4  Rel wrel 5655   Fn wfn 6533  ⟶wf 6534

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 6540  df-fn 6541  df-f 6542

This theorem is used by:  freld  6716  fssxp  6737  fimadmfoALT  6807  foconst  6811  fsn  7136  fnwelem  8145  mapsnd  8917  axdc3lem4  10534  imasless  17717  gimcnv  19486  gsumval3  20126  rngimcnv  20691  rimcnv  20722  lmimcnv  21347  mattpostpos  22774  hmeocnv  24086  metn0  24684  rlimcnp2  27299  wlkn0  30206  tocyccntz  33751  mbfresfi  38677  seff  45386  sge0cl  47484