Theorem funrel 5335

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 5320	. 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 3197   _I cid 4379   `'ccnv 4718   o. ccom 4723   Rel wrel 4724   Fun wfun 5312

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 5320

This theorem is referenced by:  0nelfun  5336  funeu  5343  nfunv  5351  funopg  5352  funssres  5360  funun  5362  fununfun  5364  fununi  5389  funcnvres2  5396  funimaexg  5405  fnrel  5419  fcoi1  5508  f1orel  5577  funbrfv  5672  funbrfv2b  5680  fvmptss2  5711  mptrcl  5719  elfvmptrab1  5731  funfvbrb  5750  fmptco  5803  funopsn  5819  funresdfunsnss  5846  elmpocl  6206  relmptopab  6213  funexw  6263  mpoxopn0yelv  6391  tfrlem6  6468  funresdfunsndc  6660  pmresg  6831  fundmen  6967  caseinl  7269  caseinr  7270  axaddf  8066  axmulf  8067  hashinfom  11012  4sqlemffi  12934  structcnvcnv  13063  lidlmex  14454  istopon  14702  eltg4i  14744  eltg3  14746  tg1  14748  tg2  14749  tgclb  14754  lmrcl  14881  1vgrex  15836  edg0iedg0g  15881  umgrnloopv  15929