ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  funrel Unicode version

Theorem funrel 5229
Description: A function is a relation. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
funrel  |-  ( Fun 
A  ->  Rel  A )

Proof of Theorem funrel
StepHypRef Expression
1 df-fun 5214 . 2  |-  ( Fun 
A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
21simplbi 274 1  |-  ( Fun 
A  ->  Rel  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3129    _I cid 4285   `'ccnv 4622    o. ccom 4627   Rel wrel 4628   Fun wfun 5206
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 5214
This theorem is referenced by:  0nelfun  5230  funeu  5237  nfunv  5245  funopg  5246  funssres  5254  funun  5256  fununi  5280  funcnvres2  5287  funimaexg  5296  fnrel  5310  fcoi1  5392  f1orel  5460  funbrfv  5550  funbrfv2b  5556  fvmptss2  5587  mptrcl  5594  elfvmptrab1  5606  funfvbrb  5625  fmptco  5678  funresdfunsnss  5715  elmpocl  6063  funexw  6107  mpoxopn0yelv  6234  tfrlem6  6311  funresdfunsndc  6501  pmresg  6670  fundmen  6800  caseinl  7084  caseinr  7085  axaddf  7855  axmulf  7856  hashinfom  10739  structcnvcnv  12458  istopon  13171  eltg4i  13215  eltg3  13217  tg1  13219  tg2  13220  tgclb  13225  lmrcl  13351
  Copyright terms: Public domain W3C validator