Theorem fnrel 5479

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

This proof depends on syntax axioms:   -> wi 4   Rel wrel 4779   Fun wfun 5371   Fn wfn 5372

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-fun 5379  df-fn 5380

This theorem is used by:  fnbr  5485  fnresdm  5492  fn0  5503  frel  5538  fcoi2  5573  f1rel  5602  f1ocnv  5652  dffn5im  5748  fnex  5937  fnexALT  6340  basmex  13464  basmexd  13465  slotm  13467  ismgmn0  13731  mgpplusg  14306  mgpbas  14309  ringidval  14349  psrelbas  15151  psradd  15155  psraddcl  15156  psrmulfval  15159  mplrcl  15176  mplbasss  15178  mpladd  15186  istps  15224  topontopn  15229  cldrcl  15294  neiss2  15334