Theorem fnrel 5371

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

Syntax hints:   -> wi 4   Rel wrel 4679   Fun wfun 5264   Fn wfn 5265

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 5272  df-fn 5273

This theorem is referenced by:  fnbr  5377  fnresdm  5384  fn0  5394  frel  5429  fcoi2  5456  f1rel  5484  f1ocnv  5534  dffn5im  5623  fnex  5805  fnexALT  6195  basmex  12833  basmexd  12834  ismgmn0  13132  psrelbas  14379  psradd  14383  psraddcl  14384  mplrcl  14398  mplbasss  14400  mpladd  14408  istps  14446  topontopn  14451  cldrcl  14516  neiss2  14556