Theorem fnrel 5428

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

Syntax hints:   -> wi 4   Rel wrel 4730   Fun wfun 5320   Fn wfn 5321

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 5328  df-fn 5329

This theorem is referenced by:  fnbr  5434  fnresdm  5441  fn0  5452  frel  5487  fcoi2  5518  f1rel  5546  f1ocnv  5596  dffn5im  5691  fnex  5876  fnexALT  6273  basmex  13160  basmexd  13161  ismgmn0  13459  psrelbas  14708  psradd  14712  psraddcl  14713  mplrcl  14727  mplbasss  14729  mpladd  14737  istps  14775  topontopn  14780  cldrcl  14845  neiss2  14885