Theorem funrel 5343

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 5328	. 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 3200   _I cid 4385   `'ccnv 4724   o. ccom 4729   Rel wrel 4730   Fun wfun 5320

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 5328

This theorem is referenced by:  0nelfun  5344  funeu  5351  nfunv  5359  funopg  5360  funssres  5369  funun  5371  fununfun  5373  fununi  5398  funcnvres2  5405  funimaexg  5414  fnrel  5428  fcoi1  5517  f1orel  5586  funbrfv  5682  funbrfv2b  5690  fvmptss2  5721  mptrcl  5729  elfvmptrab1  5741  funfvbrb  5760  fmptco  5813  funopsn  5830  funresdfunsnss  5857  elmpocl  6217  relmptopab  6224  funexw  6274  elmpom  6403  mpoxopn0yelv  6405  tfrlem6  6482  funresdfunsndc  6674  pmresg  6845  fundmen  6981  caseinl  7290  caseinr  7291  axaddf  8088  axmulf  8089  hashinfom  11041  4sqlemffi  12974  structcnvcnv  13103  lidlmex  14495  istopon  14743  eltg4i  14785  eltg3  14787  tg1  14789  tg2  14790  tgclb  14795  lmrcl  14922  1vgrex  15877  edg0iedg0g  15923  umgrnloopv  15971  edg0usgr  16104