Theorem fnrel 5333

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

Syntax hints:   -> wi 4   Rel wrel 4649   Fun wfun 5229   Fn wfn 5230

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 5237  df-fn 5238

This theorem is referenced by:  fnbr  5337  fnresdm  5344  fn0  5354  frel  5389  fcoi2  5416  f1rel  5444  f1ocnv  5493  dffn5im  5581  fnex  5758  fnexALT  6135  basmex  12570  basmexd  12571  ismgmn0  12831  istps  13984  topontopn  13989  cldrcl  14054  neiss2  14094