Theorem frel 6675

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

Syntax hints:   → wi 4  Rel wrel 5637   Fn wfn 6495  ⟶wf 6496

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 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  freld  6676  fssxp  6697  fimadmfoALT  6765  foconst  6769  fsn  7090  fnwelem  8083  mapsnd  8836  axdc3lem4  10375  imasless  17473  gimcnv  19208  gsumval3  19848  rngimcnv  20404  lmimcnv  21031  mattpostpos  22410  hmeocnv  23718  metn0  24316  rlimcnp2  26944  wlkn0  29706  cyclnumvtx  29885  tocyccntz  33237  mbfresfi  37914  rimcnv  42884  seff  44662  fresin2  45528  cncfuni  46241  fourierdlem48  46509  fourierdlem49  46510  fourierdlem113  46574  sge0cl  46736