Theorem funrel 5275

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 5260	. 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 3157   _I cid 4323   `'ccnv 4662   o. ccom 4667   Rel wrel 4668   Fun wfun 5252

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 5260

This theorem is referenced by:  0nelfun  5276  funeu  5283  nfunv  5291  funopg  5292  funssres  5300  funun  5302  fununi  5326  funcnvres2  5333  funimaexg  5342  fnrel  5356  fcoi1  5438  f1orel  5507  funbrfv  5599  funbrfv2b  5605  fvmptss2  5636  mptrcl  5644  elfvmptrab1  5656  funfvbrb  5675  fmptco  5728  funresdfunsnss  5765  elmpocl  6118  funexw  6169  mpoxopn0yelv  6297  tfrlem6  6374  funresdfunsndc  6564  pmresg  6735  fundmen  6865  caseinl  7157  caseinr  7158  axaddf  7935  axmulf  7936  hashinfom  10870  4sqlemffi  12565  structcnvcnv  12694  lidlmex  14031  istopon  14249  eltg4i  14291  eltg3  14293  tg1  14295  tg2  14296  tgclb  14301  lmrcl  14427