Theorem frel 6667

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

Syntax hints:   → wi 4  Rel wrel 5629   Fn wfn 6487  ⟶wf 6488

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 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  freld  6668  fssxp  6689  fimadmfoALT  6757  foconst  6761  fsn  7080  fnwelem  8073  mapsnd  8824  axdc3lem4  10363  imasless  17461  gimcnv  19196  gsumval3  19836  rngimcnv  20392  lmimcnv  21019  mattpostpos  22398  hmeocnv  23706  metn0  24304  rlimcnp2  26932  wlkn0  29694  cyclnumvtx  29873  tocyccntz  33226  mbfresfi  37863  rimcnv  42768  seff  44546  fresin2  45412  cncfuni  46126  fourierdlem48  46394  fourierdlem49  46395  fourierdlem113  46459  sge0cl  46621