Theorem funrel 5019

Description: A function is a relation. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
funrel	|- ( Fun A -> Rel A )

Proof of Theorem funrel

Step	Hyp	Ref	Expression
1		df-fun 5004	. 2 |- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
2	1	simplbi 268	1 |- ( Fun A -> Rel A )

Syntax hints:   -> wi 4   C_ wss 2997   _I cid 4106   `'ccnv 4427   o. ccom 4432   Rel wrel 4433   Fun wfun 4996

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115  df-fun 5004

This theorem is referenced by:  funeu  5026  nfunv  5033  funopg  5034  funssres  5042  funun  5044  fununi  5068  funcnvres2  5075  funimaexg  5084  fnrel  5098  fcoi1  5175  f1orel  5240  funbrfv  5327  funbrfv2b  5333  fvmptss2  5363  funfvbrb  5396  fmptco  5448  elmpt2cl  5824  mpt2xopn0yelv  5986  tfrlem6  6063  pmresg  6413  fundmen  6503  hashinfom  10151