Theorem frel 6718

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

This proof depends on syntax axioms:   → wi 4  Rel wrel 5671   Fn wfn 6538  ⟶wf 6539

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 6545  df-fn 6546  df-f 6547

This theorem is used by:  freld  6719  fssxp  6740  fimadmfoALT  6810  foconst  6814  fsn  7138  fnwelem  8136  mapsnd  8893  axdc3lem4  10455  imasless  17619  gimcnv  19368  gsumval3  20008  rngimcnv  20571  rimcnv  20602  lmimcnv  21225  mattpostpos  22648  hmeocnv  23956  metn0  24554  rlimcnp2  27168  wlkn0  30007  tocyccntz  33495  mbfresfi  38358  seff  45060  sge0cl  47136