Theorem frel 6050

Description: A mapping is a relation. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
frel	|- ( F : A --> B -> Rel F )

Proof of Theorem frel

Step	Hyp	Ref	Expression
1		ffn 6045	. 2 |- ( F : A --> B -> F Fn A )
2		fnrel 5989	. 2 |- ( F Fn A -> Rel F )
3	1, 2	syl 17	1 |- ( F : A --> B -> Rel F )

Syntax hints:   -> wi 4   Rel wrel 5119   Fn wfn 5883   -->wf 5884

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 386  df-fun 5890  df-fn 5891  df-f 5892

This theorem is referenced by:  fssxp  6060  foconst  6126  fsn  6402  fnwelem  7292  mapsn  7899  axdc3lem4  9275  imasless  16200  gimcnv  17709  gsumval3  18308  lmimcnv  19067  mattpostpos  20260  hmeocnv  21565  metn0  22165  rlimcnp2  24693  wlkn0  26516  mbfresfi  33456  seff  38508  fresin2  39352  mapsnd  39388  freld  39425  cncfuni  40099  fourierdlem48  40371  fourierdlem49  40372  fourierdlem113  40436  sge0cl  40598