Theorem fnrel 4997

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

Syntax hints:   -> wi 4   Rel wrel 4350   Fun wfun 4896   Fn wfn 4897

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99

This theorem depends on definitions:  df-bi 110  df-fun 4904  df-fn 4905

This theorem is referenced by:  fnbr  5001  fnresdm  5008  fn0  5018  frel  5049  fcoi2  5071  f1rel  5095  f1ocnv  5139  dffn5im  5219  fnex  5383  fnexALT  5740