Theorem frel 6673

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

Syntax hints:   → wi 4  Rel wrel 5636   Fn wfn 6493  ⟶wf 6494

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 6500  df-fn 6501  df-f 6502

This theorem is referenced by:  freld  6674  fssxp  6695  fimadmfoALT  6763  foconst  6767  fsn  7088  fnwelem  8081  mapsnd  8834  axdc3lem4  10375  imasless  17504  gimcnv  19242  gsumval3  19882  rngimcnv  20436  lmimcnv  21062  mattpostpos  22419  hmeocnv  23727  metn0  24325  rlimcnp2  26930  wlkn0  29689  cyclnumvtx  29868  tocyccntz  33205  mbfresfi  37987  rimcnv  42962  seff  44736  fresin2  45602  cncfuni  46314  fourierdlem48  46582  fourierdlem49  46583  fourierdlem113  46647  sge0cl  46809