Theorem frel 6643

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

Syntax hints:   → wi 4  Rel wrel 5613   Fn wfn 6461  ⟶wf 6462

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 397  df-fun 6468  df-fn 6469  df-f 6470

This theorem is referenced by:  freld  6644  fssxp  6666  fimadmfoALT  6737  foconst  6741  fsn  7047  fnwelem  8018  mapsnd  8724  axdc3lem4  10289  imasless  17328  gimcnv  18959  gsumval3  19583  lmimcnv  20412  mattpostpos  21686  hmeocnv  22996  metn0  23596  rlimcnp2  26199  wlkn0  28124  tocyccntz  31546  mbfresfi  35895  seff  42161  fresin2  42949  cncfuni  43677  fourierdlem48  43945  fourierdlem49  43946  fourierdlem113  44010  sge0cl  44170