Theorem frel 6712

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

Syntax hints:   → wi 4  Rel wrel 5667   Fn wfn 6532  ⟶wf 6533

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

This theorem is referenced by:  freld  6713  fssxp  6734  fimadmfoALT  6804  foconst  6808  fsn  7132  fnwelem  8127  mapsnd  8884  axdc3lem4  10437  imasless  17594  gimcnv  19337  gsumval3  19977  rngimcnv  20538  rimcnv  20567  lmimcnv  21166  mattpostpos  22580  hmeocnv  23888  metn0  24486  rlimcnp2  27097  wlkn0  29911  tocyccntz  33405  mbfresfi  38205  seff  44911  sge0cl  46987