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

Theorem funrel 5098
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 5083 . 2  |-  ( Fun 
A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
21simplbi 270 1  |-  ( Fun 
A  ->  Rel  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3037    _I cid 4170   `'ccnv 4498    o. ccom 4503   Rel wrel 4504   Fun wfun 5075
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-fun 5083
This theorem is referenced by:  0nelfun  5099  funeu  5106  nfunv  5114  funopg  5115  funssres  5123  funun  5125  fununi  5149  funcnvres2  5156  funimaexg  5165  fnrel  5179  fcoi1  5261  f1orel  5326  funbrfv  5414  funbrfv2b  5420  fvmptss2  5450  mptrcl  5457  elfvmptrab1  5469  funfvbrb  5487  fmptco  5540  funresdfunsnss  5577  elmpocl  5922  mpoxopn0yelv  6090  tfrlem6  6167  funresdfunsndc  6356  pmresg  6524  fundmen  6654  caseinl  6928  caseinr  6929  axaddf  7603  axmulf  7604  hashinfom  10417  structcnvcnv  11818  istopon  12023  eltg4i  12067  eltg3  12069  tg1  12071  tg2  12072  tgclb  12077  lmrcl  12203
  Copyright terms: Public domain W3C validator