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

Theorem funrel 5252
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 5237 . 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 3144    _I cid 4306   `'ccnv 4643    o. ccom 4648   Rel wrel 4649   Fun wfun 5229
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 5237
This theorem is referenced by:  0nelfun  5253  funeu  5260  nfunv  5268  funopg  5269  funssres  5277  funun  5279  fununi  5303  funcnvres2  5310  funimaexg  5319  fnrel  5333  fcoi1  5415  f1orel  5483  funbrfv  5574  funbrfv2b  5580  fvmptss2  5611  mptrcl  5618  elfvmptrab1  5630  funfvbrb  5649  fmptco  5702  funresdfunsnss  5739  elmpocl  6090  funexw  6136  mpoxopn0yelv  6263  tfrlem6  6340  funresdfunsndc  6530  pmresg  6701  fundmen  6831  caseinl  7119  caseinr  7120  axaddf  7896  axmulf  7897  hashinfom  10789  4sqlemffi  12427  structcnvcnv  12527  lidlmex  13788  istopon  13965  eltg4i  14007  eltg3  14009  tg1  14011  tg2  14012  tgclb  14017  lmrcl  14143
  Copyright terms: Public domain W3C validator