Theorem frel 6349

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

Syntax hints:   → wi 4  Rel wrel 5412   Fn wfn 6183  ⟶wf 6184

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 199  df-an 388  df-fun 6190  df-fn 6191  df-f 6192

This theorem is referenced by:  fssxp  6363  fimadmfoALT  6430  foconst  6432  fsn  6720  fnwelem  7630  mapsnd  8248  axdc3lem4  9673  imasless  16669  gimcnv  18178  gsumval3  18781  lmimcnv  19561  mattpostpos  20767  hmeocnv  22074  metn0  22673  rlimcnp2  25246  wlkn0  27105  mbfresfi  34376  seff  40054  fresin2  40850  freld  40917  cncfuni  41597  fourierdlem48  41868  fourierdlem49  41869  fourierdlem113  41933  sge0cl  42092