Theorem frel 6693

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

Syntax hints:   → wi 4  Rel wrel 5650   Fn wfn 6512  ⟶wf 6513

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 209  df-an 400  df-fun 6519  df-fn 6520  df-f 6521

This theorem is referenced by:  freld  6694  fssxp  6715  fimadmfoALT  6785  foconst  6789  fsn  7113  fnwelem  8106  mapsnd  8864  axdc3lem4  10407  imasless  17553  gimcnv  19290  gsumval3  19930  rngimcnv  20484  rimcnv  20513  lmimcnv  21114  mattpostpos  22494  hmeocnv  23802  metn0  24400  rlimcnp2  27008  wlkn0  29767  cyclnumvtx  29946  tocyccntz  33285  mbfresfi  38129  seff  44849  sge0cl  46919