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  5875  fnexALT  6272  basmex  13141  basmexd  13142  ismgmn0  13440  psrelbas  14688  psradd  14692  psraddcl  14693  mplrcl  14707  mplbasss  14709  mpladd  14717  istps  14755  topontopn  14760  cldrcl  14825  neiss2  14865