Theorem fnrel 5381

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

Syntax hints:   -> wi 4   Rel wrel 4688   Fun wfun 5274   Fn wfn 5275

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 5282  df-fn 5283

This theorem is referenced by:  fnbr  5387  fnresdm  5394  fn0  5405  frel  5440  fcoi2  5469  f1rel  5497  f1ocnv  5547  dffn5im  5637  fnex  5819  fnexALT  6209  basmex  12966  basmexd  12967  ismgmn0  13265  psrelbas  14512  psradd  14516  psraddcl  14517  mplrcl  14531  mplbasss  14533  mpladd  14541  istps  14579  topontopn  14584  cldrcl  14649  neiss2  14689