Theorem frel 6723

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

Syntax hints:   → wi 4  Rel wrel 5682   Fn wfn 6539  ⟶wf 6540

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 206  df-an 398  df-fun 6546  df-fn 6547  df-f 6548

This theorem is referenced by:  freld  6724  fssxp  6746  fimadmfoALT  6817  foconst  6821  fsn  7133  fnwelem  8117  mapsnd  8880  axdc3lem4  10448  imasless  17486  gimcnv  19141  gsumval3  19775  lmimcnv  20678  mattpostpos  21956  hmeocnv  23266  metn0  23866  rlimcnp2  26471  wlkn0  28878  tocyccntz  32303  mbfresfi  36534  rimcnv  41092  seff  43068  fresin2  43868  cncfuni  44602  fourierdlem48  44870  fourierdlem49  44871  fourierdlem113  44935  sge0cl  45097  rngimcnv  46705