Theorem funrel 4943

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 4928	. 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 2974   _I cid 4045   `'ccnv 4364   o. ccom 4369   Rel wrel 4370   Fun wfun 4920

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 4928

This theorem is referenced by:  funeu  4950  nfunv  4957  funopg  4958  funssres  4966  funun  4968  fununi  4992  funcnvres2  4999  funimaexg  5008  fnrel  5022  fcoi1  5095  f1orel  5154  funbrfv  5238  funbrfv2b  5244  fvmptss2  5273  funfvbrb  5306  fmptco  5356  elmpt2cl  5723  mpt2xopn0yelv  5882  tfrlem6  5959  fundmen  6345  sizeinf  9791