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

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

Proof of Theorem funrel
StepHypRef Expression
1 df-fun 4847 . 2  Fun  Rel  o.  `'  C_  _I
21simplbi 259 1  Fun  Rel
Colors of variables: wff set class
Syntax hints:   wi 4    C_ wss 2911    _I cid 4016   `'ccnv 4287    o. ccom 4292   Rel wrel 4293   Fun wfun 4839
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110  df-fun 4847
This theorem is referenced by:  funeu  4869  nfunv  4876  funopg  4877  funssres  4885  funun  4887  fununi  4910  funcnvres2  4917  funimaexg  4926  fnrel  4940  fcoi1  5013  f1orel  5072  funbrfv  5155  funbrfv2b  5161  fvmptss2  5190  funfvbrb  5223  fmptco  5273  elmpt2cl  5640  mpt2xopn0yelv  5795  tfrlem6  5873  fundmen  6222
  Copyright terms: Public domain W3C validator