Theorem fnrel 5306

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

Syntax hints:   -> wi 4   Rel wrel 4625   Fun wfun 5202   Fn wfn 5203

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 5210  df-fn 5211

This theorem is referenced by:  fnbr  5310  fnresdm  5317  fn0  5327  frel  5362  fcoi2  5389  f1rel  5417  f1ocnv  5466  dffn5im  5553  fnex  5730  fnexALT  6102  basmex  12487  basmexd  12488  ismgmn0  12643  istps  13101  topontopn  13106  cldrcl  13173  neiss2  13213