Theorem fnrel 5425

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

Syntax hints:   -> wi 4   Rel wrel 4728   Fun wfun 5318   Fn wfn 5319

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 5326  df-fn 5327

This theorem is referenced by:  fnbr  5431  fnresdm  5438  fn0  5449  frel  5484  fcoi2  5515  f1rel  5543  f1ocnv  5593  dffn5im  5687  fnex  5871  fnexALT  6268  basmex  13132  basmexd  13133  ismgmn0  13431  psrelbas  14679  psradd  14683  psraddcl  14684  mplrcl  14698  mplbasss  14700  mpladd  14708  istps  14746  topontopn  14751  cldrcl  14816  neiss2  14856