Theorem funrel 5369

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 5354	. 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 3211   _I cid 4409   `'ccnv 4748   o. ccom 4753   Rel wrel 4754   Fun wfun 5346

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 5354

This theorem is referenced by:  0nelfun  5370  funeu  5377  nfunv  5385  funopg  5386  funssres  5395  funun  5397  fununfun  5399  fununi  5424  funcnvres2  5431  funimaexg  5440  fnrel  5454  fcoi1  5547  f1orel  5617  funbrfv  5713  funbrfv2b  5721  fvmptss2  5752  mptrcl  5760  elfvmptrab1  5772  funfvbrb  5791  fmptco  5843  funopsn  5860  funresdfunsnss  5887  elmpocl  6249  relmptopab  6256  funexw  6305  elmpom  6434  mpoxopn0yelv  6470  tfrlem6  6547  funresdfunsndc  6739  pmresg  6910  fundmen  7047  caseinl  7382  caseinr  7383  axaddf  8183  axmulf  8184  hashinfom  11141  4sqlemffi  13094  structcnvcnv  13228  lidlmex  14623  istopon  14878  eltg4i  14920  eltg3  14922  tg1  14924  tg2  14925  tgclb  14930  lmrcl  15057  1vgrex  16015  edg0iedg0g  16061  umgrnloopv  16109  edg0usgr  16242