Theorem frel 6695

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

Syntax hints:   → wi 4  Rel wrel 5645   Fn wfn 6508  ⟶wf 6509

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 6515  df-fn 6516  df-f 6517

This theorem is referenced by:  freld  6696  fssxp  6717  fimadmfoALT  6785  foconst  6789  fsn  7109  fnwelem  8112  mapsnd  8861  axdc3lem4  10412  imasless  17509  gimcnv  19205  gsumval3  19843  rngimcnv  20371  lmimcnv  20980  mattpostpos  22347  hmeocnv  23655  metn0  24254  rlimcnp2  26882  wlkn0  29555  cyclnumvtx  29736  tocyccntz  33107  mbfresfi  37655  rimcnv  42498  seff  44291  fresin2  45159  cncfuni  45877  fourierdlem48  46145  fourierdlem49  46146  fourierdlem113  46210  sge0cl  46372