Theorem fnrel 5418

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

Syntax hints:   -> wi 4   Rel wrel 4723   Fun wfun 5311   Fn wfn 5312

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 5319  df-fn 5320

This theorem is referenced by:  fnbr  5424  fnresdm  5431  fn0  5442  frel  5477  fcoi2  5506  f1rel  5534  f1ocnv  5584  dffn5im  5678  fnex  5860  fnexALT  6254  basmex  13087  basmexd  13088  ismgmn0  13386  psrelbas  14633  psradd  14637  psraddcl  14638  mplrcl  14652  mplbasss  14654  mpladd  14662  istps  14700  topontopn  14705  cldrcl  14770  neiss2  14810