Theorem fnrel 5459

Description: A function with domain is a relation. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
fnrel	|- ( F Fn A -> Rel F )

Proof of Theorem fnrel

Step	Hyp	Ref	Expression
1		fnfun 5458	. 2 |- ( F Fn A -> Fun F )
2		funrel 5374	. 2 |- ( Fun F -> Rel F )
3	1, 2	syl 14	1 |- ( F Fn A -> Rel F )

Syntax hints:   -> wi 4   Rel wrel 4759   Fun wfun 5351   Fn wfn 5352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-fun 5359  df-fn 5360

This theorem is referenced by:  fnbr  5465  fnresdm  5472  fn0  5483  frel  5518  fcoi2  5553  f1rel  5582  f1ocnv  5632  dffn5im  5727  fnex  5911  fnexALT  6313  basmex  13356  basmexd  13357  ismgmn0  13621  psrelbas  14956  psradd  14960  psraddcl  14961  mplrcl  14975  mplbasss  14977  mpladd  14985  istps  15023  topontopn  15028  cldrcl  15093  neiss2  15133