Theorem fnrel 5311

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

Syntax hints:   -> wi 4   Rel wrel 4629   Fun wfun 5207   Fn wfn 5208

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 5215  df-fn 5216

This theorem is referenced by:  fnbr  5315  fnresdm  5322  fn0  5332  frel  5367  fcoi2  5394  f1rel  5422  f1ocnv  5471  dffn5im  5558  fnex  5735  fnexALT  6107  basmex  12511  basmexd  12512  ismgmn0  12707  istps  13312  topontopn  13317  cldrcl  13384  neiss2  13424