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  13461  basmexd  13462  slotm  13464  ismgmn0  13727  mgpplusg  14271  mgpbas  14274  ringidval  14314  psrelbas  15115  psradd  15119  psraddcl  15120  mplrcl  15134  mplbasss  15136  mpladd  15144  istps  15182  topontopn  15187  cldrcl  15252  neiss2  15292