Theorem frel 6661

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

Syntax hints:   → wi 4  Rel wrel 5628   Fn wfn 6481  ⟶wf 6482

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 6488  df-fn 6489  df-f 6490

This theorem is referenced by:  freld  6662  fssxp  6683  fimadmfoALT  6751  foconst  6755  fsn  7073  fnwelem  8071  mapsnd  8820  axdc3lem4  10366  imasless  17462  gimcnv  19164  gsumval3  19804  rngimcnv  20359  lmimcnv  20989  mattpostpos  22357  hmeocnv  23665  metn0  24264  rlimcnp2  26892  wlkn0  29584  cyclnumvtx  29763  tocyccntz  33099  mbfresfi  37645  rimcnv  42490  seff  44282  fresin2  45150  cncfuni  45868  fourierdlem48  46136  fourierdlem49  46137  fourierdlem113  46201  sge0cl  46363