Theorem fnrel 5474

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

Syntax hints:   -> wi 4   Rel wrel 4774   Fun wfun 5366   Fn wfn 5367

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 5374  df-fn 5375

This theorem is referenced by:  fnbr  5480  fnresdm  5487  fn0  5498  frel  5533  fcoi2  5568  f1rel  5597  f1ocnv  5647  dffn5im  5742  fnex  5928  fnexALT  6330  basmex  13390  basmexd  13391  ismgmn0  13655  psrelbas  14989  psradd  14993  psraddcl  14994  mplrcl  15008  mplbasss  15010  mpladd  15018  istps  15056  topontopn  15061  cldrcl  15126  neiss2  15166