Theorem frel 6693

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

Syntax hints:   → wi 4  Rel wrel 5643   Fn wfn 6506  ⟶wf 6507

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 207  df-an 396  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  freld  6694  fssxp  6715  fimadmfoALT  6783  foconst  6787  fsn  7107  fnwelem  8110  mapsnd  8859  axdc3lem4  10406  imasless  17503  gimcnv  19199  gsumval3  19837  rngimcnv  20365  lmimcnv  20974  mattpostpos  22341  hmeocnv  23649  metn0  24248  rlimcnp2  26876  wlkn0  29549  cyclnumvtx  29730  tocyccntz  33101  mbfresfi  37660  rimcnv  42505  seff  44298  fresin2  45166  cncfuni  45884  fourierdlem48  46152  fourierdlem49  46153  fourierdlem113  46217  sge0cl  46379