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  14313  mgpbas  14316  ringidval  14356  psrelbas  15158  psradd  15162  psraddcl  15163  psrmulfval  15166  mplrcl  15184  mplbasss  15186  mpladd  15194  istps  15232  topontopn  15237  cldrcl  15302  neiss2  15342