Theorem frel 6512

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

Syntax hints:   → wi 4  Rel wrel 5553   Fn wfn 6343  ⟶wf 6344

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 209  df-an 399  df-fun 6350  df-fn 6351  df-f 6352

This theorem is referenced by:  fssxp  6527  fimadmfoALT  6594  foconst  6596  fsn  6890  fnwelem  7818  mapsnd  8443  axdc3lem4  9868  imasless  16808  gimcnv  18402  gsumval3  19022  lmimcnv  19834  mattpostpos  21058  hmeocnv  22365  metn0  22965  rlimcnp2  25542  wlkn0  27400  tocyccntz  30807  mbfresfi  34973  seff  40715  fresin2  41502  freld  41567  cncfuni  42243  fourierdlem48  42513  fourierdlem49  42514  fourierdlem113  42578  sge0cl  42737