Theorem funrel 5350

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 5335	. 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 3201   _I cid 4391   `'ccnv 4730   o. ccom 4735   Rel wrel 4736   Fun wfun 5327

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 5335

This theorem is referenced by:  0nelfun  5351  funeu  5358  nfunv  5366  funopg  5367  funssres  5376  funun  5378  fununfun  5380  fununi  5405  funcnvres2  5412  funimaexg  5421  fnrel  5435  fcoi1  5525  f1orel  5595  funbrfv  5691  funbrfv2b  5699  fvmptss2  5730  mptrcl  5738  elfvmptrab1  5750  funfvbrb  5769  fmptco  5821  funopsn  5838  funresdfunsnss  5865  elmpocl  6227  relmptopab  6234  funexw  6283  elmpom  6412  mpoxopn0yelv  6448  tfrlem6  6525  funresdfunsndc  6717  pmresg  6888  fundmen  7024  caseinl  7333  caseinr  7334  axaddf  8131  axmulf  8132  hashinfom  11086  4sqlemffi  13032  structcnvcnv  13161  lidlmex  14554  istopon  14807  eltg4i  14849  eltg3  14851  tg1  14853  tg2  14854  tgclb  14859  lmrcl  14986  1vgrex  15944  edg0iedg0g  15990  umgrnloopv  16038  edg0usgr  16171