Theorem frel 6701

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

Syntax hints:   → wi 4  Rel wrel 5657   Fn wfn 6520  ⟶wf 6521

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 6527  df-fn 6528  df-f 6529

This theorem is referenced by:  freld  6702  fssxp  6723  fimadmfoALT  6793  foconst  6797  fsn  7121  fnwelem  8115  mapsnd  8872  axdc3lem4  10425  imasless  17584  gimcnv  19328  gsumval3  19968  rngimcnv  20529  rimcnv  20558  lmimcnv  21157  mattpostpos  22572  hmeocnv  23880  metn0  24478  rlimcnp2  27089  wlkn0  29879  cyclnumvtx  30058  tocyccntz  33377  mbfresfi  38177  seff  44883  sge0cl  46953