Theorem frel 6741

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

Syntax hints:   → wi 4  Rel wrel 5690   Fn wfn 6556  ⟶wf 6557

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 6563  df-fn 6564  df-f 6565

This theorem is referenced by:  freld  6742  fssxp  6763  fimadmfoALT  6831  foconst  6835  fsn  7155  fnwelem  8156  mapsnd  8926  axdc3lem4  10493  imasless  17585  gimcnv  19285  gsumval3  19925  rngimcnv  20456  lmimcnv  21066  mattpostpos  22460  hmeocnv  23770  metn0  24370  rlimcnp2  27009  wlkn0  29639  cyclnumvtx  29820  tocyccntz  33164  mbfresfi  37673  rimcnv  42527  seff  44328  fresin2  45177  cncfuni  45901  fourierdlem48  46169  fourierdlem49  46170  fourierdlem113  46234  sge0cl  46396