Theorem funrel 5389

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 5374	. 2 |- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
2	1	simplbi 274	1 |- ( Fun A -> Rel A )

Syntax hints:   -> wi 4   C_ wss 3220   _I cid 4428   `'ccnv 4768   o. ccom 4773   Rel wrel 4774   Fun wfun 5366

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 5374

This theorem is referenced by:  0nelfun  5390  funeu  5397  nfunv  5405  funopg  5406  funssres  5415  funun  5417  fununfun  5419  fununi  5444  funcnvres2  5451  funimaexg  5460  fnrel  5474  fcoi1  5567  f1orel  5637  funbrfv  5733  funbrfv2b  5741  fvmptss2  5774  mptrcl  5782  elfvmptrab1  5794  funfvbrb  5813  fmptco  5865  funopsn  5882  funresdfunsnss  5909  elmpocl  6274  relmptopab  6281  funexw  6331  elmpom  6464  mpoxopn0yelv  6500  tfrlem6  6577  funresdfunsndc  6769  pmresg  6947  fundmen  7084  caseinl  7421  caseinr  7422  axaddf  8225  axmulf  8226  hashinfom  11195  4sqlemffi  13153  structcnvcnv  13346  lidlmex  14784  istopon  15037  eltg4i  15079  eltg3  15081  tg1  15083  tg2  15084  tgclb  15089  lmrcl  15216  1vgrex  16175  edg0iedg0g  16221  umgrnloopv  16269  edg0usgr  16402