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  5509  f1rel  5537  f1ocnv  5587  dffn5im  5681  fnex  5865  fnexALT  6262  basmex  13107  basmexd  13108  ismgmn0  13406  psrelbas  14654  psradd  14658  psraddcl  14659  mplrcl  14673  mplbasss  14675  mpladd  14683  istps  14721  topontopn  14726  cldrcl  14791  neiss2  14831