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

Theorem funrel 4943
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 4928 . 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 2974    _I cid 4045   `'ccnv 4364    o. ccom 4369   Rel wrel 4370   Fun wfun 4920
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 4928
This theorem is referenced by:  funeu  4950  nfunv  4957  funopg  4958  funssres  4966  funun  4968  fununi  4992  funcnvres2  4999  funimaexg  5008  fnrel  5022  fcoi1  5095  f1orel  5154  funbrfv  5238  funbrfv2b  5244  fvmptss2  5273  funfvbrb  5306  fmptco  5356  elmpt2cl  5723  mpt2xopn0yelv  5882  tfrlem6  5959  fundmen  6345  sizeinf  9791
  Copyright terms: Public domain W3C validator