Theorem fnrel 5454

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

Syntax hints:   -> wi 4   Rel wrel 4754   Fun wfun 5346   Fn wfn 5347

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 5354  df-fn 5355

This theorem is referenced by:  fnbr  5460  fnresdm  5467  fn0  5478  frel  5513  fcoi2  5548  f1rel  5577  f1ocnv  5627  dffn5im  5722  fnex  5906  fnexALT  6304  basmex  13272  basmexd  13273  ismgmn0  13571  psrelbas  14830  psradd  14834  psraddcl  14835  mplrcl  14849  mplbasss  14851  mpladd  14859  istps  14897  topontopn  14902  cldrcl  14967  neiss2  15007