Theorem funrel 5341

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 5326	. 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 3198   _I cid 4383   `'ccnv 4722   o. ccom 4727   Rel wrel 4728   Fun wfun 5318

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 5326

This theorem is referenced by:  0nelfun  5342  funeu  5349  nfunv  5357  funopg  5358  funssres  5366  funun  5368  fununfun  5370  fununi  5395  funcnvres2  5402  funimaexg  5411  fnrel  5425  fcoi1  5514  f1orel  5583  funbrfv  5678  funbrfv2b  5686  fvmptss2  5717  mptrcl  5725  elfvmptrab1  5737  funfvbrb  5756  fmptco  5809  funopsn  5825  funresdfunsnss  5852  elmpocl  6212  relmptopab  6219  funexw  6269  elmpom  6398  mpoxopn0yelv  6400  tfrlem6  6477  funresdfunsndc  6669  pmresg  6840  fundmen  6976  caseinl  7281  caseinr  7282  axaddf  8078  axmulf  8079  hashinfom  11030  4sqlemffi  12959  structcnvcnv  13088  lidlmex  14479  istopon  14727  eltg4i  14769  eltg3  14771  tg1  14773  tg2  14774  tgclb  14779  lmrcl  14906  1vgrex  15861  edg0iedg0g  15907  umgrnloopv  15955  edg0usgr  16086