Theorem fnrel 5435

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

Syntax hints:   -> wi 4   Rel wrel 4736   Fun wfun 5327   Fn wfn 5328

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 5335  df-fn 5336

This theorem is referenced by:  fnbr  5441  fnresdm  5448  fn0  5459  frel  5494  fcoi2  5526  f1rel  5555  f1ocnv  5605  dffn5im  5700  fnex  5884  fnexALT  6282  basmex  13205  basmexd  13206  ismgmn0  13504  psrelbas  14759  psradd  14763  psraddcl  14764  mplrcl  14778  mplbasss  14780  mpladd  14788  istps  14826  topontopn  14831  cldrcl  14896  neiss2  14936