Theorem funrel 5135

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 5120	. 2 |- ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
2	1	simplbi 272	1 |- ( Fun A -> Rel A )

Syntax hints:   -> wi 4   C_ wss 3066   _I cid 4205   `'ccnv 4533   o. ccom 4538   Rel wrel 4539   Fun wfun 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-fun 5120

This theorem is referenced by:  0nelfun  5136  funeu  5143  nfunv  5151  funopg  5152  funssres  5160  funun  5162  fununi  5186  funcnvres2  5193  funimaexg  5202  fnrel  5216  fcoi1  5298  f1orel  5363  funbrfv  5453  funbrfv2b  5459  fvmptss2  5489  mptrcl  5496  elfvmptrab1  5508  funfvbrb  5526  fmptco  5579  funresdfunsnss  5616  elmpocl  5961  mpoxopn0yelv  6129  tfrlem6  6206  funresdfunsndc  6395  pmresg  6563  fundmen  6693  caseinl  6969  caseinr  6970  axaddf  7669  axmulf  7670  hashinfom  10517  structcnvcnv  11964  istopon  12169  eltg4i  12213  eltg3  12215  tg1  12217  tg2  12218  tgclb  12223  lmrcl  12349