Theorem fnrel 5419

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 5418	. 2 |- ( F Fn A -> Fun F )
2		funrel 5335	. 2 |- ( Fun F -> Rel F )
3	1, 2	syl 14	1 |- ( F Fn A -> Rel F )

Syntax hints:   -> wi 4   Rel wrel 4724   Fun wfun 5312   Fn wfn 5313

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 5320  df-fn 5321

This theorem is referenced by:  fnbr  5425  fnresdm  5432  fn0  5443  frel  5478  fcoi2  5507  f1rel  5535  f1ocnv  5585  dffn5im  5679  fnex  5861  fnexALT  6256  basmex  13092  basmexd  13093  ismgmn0  13391  psrelbas  14639  psradd  14643  psraddcl  14644  mplrcl  14658  mplbasss  14660  mpladd  14668  istps  14706  topontopn  14711  cldrcl  14776  neiss2  14816