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

Theorem funrel 5019
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 5004 . 2  |-  ( Fun 
A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
21simplbi 268 1  |-  ( Fun 
A  ->  Rel  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 2997    _I cid 4106   `'ccnv 4427    o. ccom 4432   Rel wrel 4433   Fun wfun 4996
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-fun 5004
This theorem is referenced by:  funeu  5026  nfunv  5033  funopg  5034  funssres  5042  funun  5044  fununi  5068  funcnvres2  5075  funimaexg  5084  fnrel  5098  fcoi1  5175  f1orel  5240  funbrfv  5327  funbrfv2b  5333  fvmptss2  5363  funfvbrb  5396  fmptco  5448  elmpt2cl  5824  mpt2xopn0yelv  5986  tfrlem6  6063  pmresg  6413  fundmen  6503  hashinfom  10151
  Copyright terms: Public domain W3C validator