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  12862  basmexd  12863  ismgmn0  13161  psrelbas  14408  psradd  14412  psraddcl  14413  mplrcl  14427  mplbasss  14429  mpladd  14437  istps  14475  topontopn  14480  cldrcl  14545  neiss2  14585