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 𝐹)

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

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

This theorem is used by:  freld  6713  fssxp  6734  fimadmfoALT  6804  foconst  6808  fsn  7133  fnwelem  8133  mapsnd  8897  axdc3lem4  10459  imasless  17632  gimcnv  19400  gsumval3  20040  rngimcnv  20603  rimcnv  20634  lmimcnv  21257  mattpostpos  22682  hmeocnv  23994  metn0  24592  rlimcnp2  27211  wlkn0  30088  tocyccntz  33592  mbfresfi  38423  seff  45141  sge0cl  47217