Theorem frel 6713

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

Syntax hints:   → wi 4  Rel wrel 5668   Fn wfn 6533  ⟶wf 6534

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 210  df-an 401  df-fun 6540  df-fn 6541  df-f 6542

This theorem is referenced by:  freld  6714  fssxp  6735  fimadmfoALT  6805  foconst  6809  fsn  7133  fnwelem  8128  mapsnd  8885  axdc3lem4  10438  imasless  17595  gimcnv  19338  gsumval3  19978  rngimcnv  20539  rimcnv  20568  lmimcnv  21169  mattpostpos  22592  hmeocnv  23900  metn0  24498  rlimcnp2  27109  wlkn0  29948  tocyccntz  33442  mbfresfi  38295  seff  44999  sge0cl  47075