Theorem funrel 4939

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 4924	. 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 2973   _I cid 4043   `'ccnv 4362   o. ccom 4367   Rel wrel 4368   Fun wfun 4916

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 4924

This theorem is referenced by:  funeu  4946  nfunv  4953  funopg  4954  funssres  4962  funun  4964  fununi  4987  funcnvres2  4994  funimaexg  5003  fnrel  5017  fcoi1  5090  f1orel  5149  funbrfv  5233  funbrfv2b  5239  fvmptss2  5268  funfvbrb  5301  fmptco  5351  elmpt2cl  5718  mpt2xopn0yelv  5877  tfrlem6  5955  fundmen  6309