Theorem frel 5963

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

Syntax hints:   → wi 4  Rel wrel 5043   Fn wfn 5799  ⟶wf 5800

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 196  df-an 385  df-fun 5806  df-fn 5807  df-f 5808

This theorem is referenced by:  fssxp  5973  foconst  6039  fsn  6308  fnwelem  7179  mapsn  7785  axdc3lem4  9158  imasless  16023  gimcnv  17532  gsumval3  18131  lmimcnv  18888  mattpostpos  20079  hmeocnv  21375  metn0  21975  rlimcnp2  24493  wlkn0  26055  usgravd00  26446  mbfresfi  32626  seff  37530  fresin2  38347  mapsnd  38383  freld  38420  cncfuni  38772  fourierdlem48  39047  fourierdlem49  39048  fourierdlem113  39112  sge0cl  39274  1wlkn0  40825