Theorem funrel 5334

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 5319	. 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 3197   _I cid 4378   `'ccnv 4717   o. ccom 4722   Rel wrel 4723   Fun wfun 5311

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 5319

This theorem is referenced by:  0nelfun  5335  funeu  5342  nfunv  5350  funopg  5351  funssres  5359  funun  5361  fununfun  5363  fununi  5388  funcnvres2  5395  funimaexg  5404  fnrel  5418  fcoi1  5505  f1orel  5574  funbrfv  5669  funbrfv2b  5677  fvmptss2  5708  mptrcl  5716  elfvmptrab1  5728  funfvbrb  5747  fmptco  5800  funopsn  5816  funresdfunsnss  5841  elmpocl  6199  funexw  6255  mpoxopn0yelv  6383  tfrlem6  6460  funresdfunsndc  6650  pmresg  6821  fundmen  6957  caseinl  7254  caseinr  7255  axaddf  8051  axmulf  8052  hashinfom  10995  4sqlemffi  12914  structcnvcnv  13043  lidlmex  14433  istopon  14681  eltg4i  14723  eltg3  14725  tg1  14727  tg2  14728  tgclb  14733  lmrcl  14859  1vgrex  15815  edg0iedg0g  15860  umgrnloopv  15908