Theorem frel 6696

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

Syntax hints:   → wi 4  Rel wrel 5646   Fn wfn 6509  ⟶wf 6510

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 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  freld  6697  fssxp  6718  fimadmfoALT  6786  foconst  6790  fsn  7110  fnwelem  8113  mapsnd  8862  axdc3lem4  10413  imasless  17510  gimcnv  19206  gsumval3  19844  rngimcnv  20372  lmimcnv  20981  mattpostpos  22348  hmeocnv  23656  metn0  24255  rlimcnp2  26883  wlkn0  29556  cyclnumvtx  29737  tocyccntz  33108  mbfresfi  37667  rimcnv  42512  seff  44305  fresin2  45173  cncfuni  45891  fourierdlem48  46159  fourierdlem49  46160  fourierdlem113  46224  sge0cl  46386