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  13412  basmexd  13413  slotm  13415  ismgmn0  13678  mgpplusg  14222  mgpbas  14225  ringidval  14265  psrelbas  15066  psradd  15070  psraddcl  15071  mplrcl  15085  mplbasss  15087  mpladd  15095  istps  15133  topontopn  15138  cldrcl  15203  neiss2  15243