Theorem frel 6528

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

Syntax hints:   → wi 4  Rel wrel 5541   Fn wfn 6353  ⟶wf 6354

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 210  df-an 400  df-fun 6360  df-fn 6361  df-f 6362

This theorem is referenced by:  freld  6529  fssxp  6551  fimadmfoALT  6622  foconst  6626  fsn  6928  fnwelem  7876  mapsnd  8545  axdc3lem4  10032  imasless  16999  gimcnv  18625  gsumval3  19246  lmimcnv  20058  mattpostpos  21305  hmeocnv  22613  metn0  23212  rlimcnp2  25803  wlkn0  27662  tocyccntz  31084  mbfresfi  35509  seff  41541  fresin2  42322  cncfuni  43045  fourierdlem48  43313  fourierdlem49  43314  fourierdlem113  43378  sge0cl  43537