Theorem funrel 5285

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 5270	. 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 3165   _I cid 4333   `'ccnv 4672   o. ccom 4677   Rel wrel 4678   Fun wfun 5262

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 5270

This theorem is referenced by:  0nelfun  5286  funeu  5293  nfunv  5301  funopg  5302  funssres  5310  funun  5312  fununi  5336  funcnvres2  5343  funimaexg  5352  fnrel  5366  fcoi1  5450  f1orel  5519  funbrfv  5611  funbrfv2b  5617  fvmptss2  5648  mptrcl  5656  elfvmptrab1  5668  funfvbrb  5687  fmptco  5740  funresdfunsnss  5777  elmpocl  6131  funexw  6187  mpoxopn0yelv  6315  tfrlem6  6392  funresdfunsndc  6582  pmresg  6753  fundmen  6883  caseinl  7175  caseinr  7176  axaddf  7963  axmulf  7964  hashinfom  10904  4sqlemffi  12638  structcnvcnv  12767  lidlmex  14155  istopon  14403  eltg4i  14445  eltg3  14447  tg1  14449  tg2  14450  tgclb  14455  lmrcl  14581