Theorem frel 6737

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

This proof depends on syntax axioms:   → wi 4  Rel wrel 5660   Fn wfn 6553  ⟶wf 6554

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fun 6560  df-fn 6561  df-f 6562

This theorem is used by:  freld  6738  fssxp  6759  fimadmfoALT  6829  foconst  6833  fsn  7160  fnwelem  8170  mapsnd  8942  axdc3lem4  10558  imasless  17741  gimcnv  19510  gsumval3  20151  rngimcnv  20716  rimcnv  20747  lmimcnv  21372  mattpostpos  22799  hmeocnv  24111  metn0  24709  rlimcnp2  27324  wlkn0  30231  tocyccntz  33775  mbfresfi  38776  seff  45485  sge0cl  47596