MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frel Structured version   Visualization version   GIF version

Theorem frel 6211
Description: A mapping is a relation. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
frel (𝐹:𝐴𝐵 → Rel 𝐹)

Proof of Theorem frel
StepHypRef Expression
1 ffn 6206 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
2 fnrel 6150 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
31, 2syl 17 1 (𝐹:𝐴𝐵 → Rel 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  Rel wrel 5271   Fn wfn 6044  wf 6045
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 197  df-an 385  df-fun 6051  df-fn 6052  df-f 6053
This theorem is referenced by:  fssxp  6221  foconst  6287  fsn  6565  fnwelem  7460  mapsn  8065  axdc3lem4  9467  imasless  16402  gimcnv  17910  gsumval3  18508  lmimcnv  19269  mattpostpos  20462  hmeocnv  21767  metn0  22366  rlimcnp2  24892  wlkn0  26726  mbfresfi  33769  seff  39010  fresin2  39851  mapsnd  39887  freld  39924  cncfuni  40602  fourierdlem48  40874  fourierdlem49  40875  fourierdlem113  40939  sge0cl  41101
  Copyright terms: Public domain W3C validator