Theorem funrel 5374

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 5359	. 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 3214   _I cid 4414   `'ccnv 4753   o. ccom 4758   Rel wrel 4759   Fun wfun 5351

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 5359

This theorem is referenced by:  0nelfun  5375  funeu  5382  nfunv  5390  funopg  5391  funssres  5400  funun  5402  fununfun  5404  fununi  5429  funcnvres2  5436  funimaexg  5445  fnrel  5459  fcoi1  5552  f1orel  5622  funbrfv  5718  funbrfv2b  5726  fvmptss2  5757  mptrcl  5765  elfvmptrab1  5777  funfvbrb  5796  fmptco  5848  funopsn  5865  funresdfunsnss  5892  elmpocl  6257  relmptopab  6264  funexw  6314  elmpom  6447  mpoxopn0yelv  6483  tfrlem6  6560  funresdfunsndc  6752  pmresg  6923  fundmen  7060  caseinl  7395  caseinr  7396  axaddf  8199  axmulf  8200  hashinfom  11166  4sqlemffi  13119  structcnvcnv  13312  lidlmex  14749  istopon  15004  eltg4i  15046  eltg3  15048  tg1  15050  tg2  15051  tgclb  15056  lmrcl  15183  1vgrex  16141  edg0iedg0g  16187  umgrnloopv  16235  edg0usgr  16368