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 5693   Fn wfn 6557  ⟶wf 6558

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

This theorem is referenced by:  freld  6742  fssxp  6763  fimadmfoALT  6831  foconst  6835  fsn  7154  fnwelem  8154  mapsnd  8924  axdc3lem4  10490  imasless  17586  gimcnv  19297  gsumval3  19939  rngimcnv  20472  lmimcnv  21083  mattpostpos  22475  hmeocnv  23785  metn0  24385  rlimcnp2  27023  wlkn0  29653  tocyccntz  33146  mbfresfi  37652  rimcnv  42503  seff  44304  fresin2  45114  cncfuni  45841  fourierdlem48  46109  fourierdlem49  46110  fourierdlem113  46174  sge0cl  46336