Theorem funrel 5252

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 5237	. 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 3144   _I cid 4306   `'ccnv 4643   o. ccom 4648   Rel wrel 4649   Fun wfun 5229

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 5237

This theorem is referenced by:  0nelfun  5253  funeu  5260  nfunv  5268  funopg  5269  funssres  5277  funun  5279  fununi  5303  funcnvres2  5310  funimaexg  5319  fnrel  5333  fcoi1  5415  f1orel  5483  funbrfv  5574  funbrfv2b  5580  fvmptss2  5611  mptrcl  5618  elfvmptrab1  5630  funfvbrb  5649  fmptco  5702  funresdfunsnss  5739  elmpocl  6090  funexw  6136  mpoxopn0yelv  6263  tfrlem6  6340  funresdfunsndc  6530  pmresg  6701  fundmen  6831  caseinl  7119  caseinr  7120  axaddf  7896  axmulf  7897  hashinfom  10789  4sqlemffi  12427  structcnvcnv  12527  lidlmex  13788  istopon  13965  eltg4i  14007  eltg3  14009  tg1  14011  tg2  14012  tgclb  14017  lmrcl  14143