Theorem fnrel 4511

Description: A function with domain is a relation.

Assertion

Ref	Expression
fnrel	|- (F Fn A -> Rel F)

Proof of Theorem fnrel

Step	Hyp	Ref	Expression
1		fnfun 4510	. 2 |- (F Fn A -> Fun F)
2		funrel 4438	. 2 |- (Fun F -> Rel F)
3	1, 2	syl 12	1 |- (F Fn A -> Rel F)

Syntax hints:   -> wi 3  Rel wrel 3991  Fun wfun 3992   Fn wfn 3993

This theorem is referenced by:  fnbr 4515  fnresdm 4522  fn0 4532  fn0OLD 4533  fnex 4535  fnexALT 4536  frel 4566  fcoi1OLD 4585  fcoi2 4586  f1ocnv 4651  dffn5 4717  fnsnfv 4728  eqfnfv 4766  fconst5 4824  tz7.48-2 5166  bnj142 12474  bnj65 13202

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242  df-fun 4008  df-fn 4009

Copyright terms: Public domain