MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funrel Unicode version

Theorem funrel 5351
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 5336 . 2  |-  ( Fun 
A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
21simplbi 446 1  |-  ( Fun 
A  ->  Rel  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3228    _I cid 4383   `'ccnv 4767    o. ccom 4772   Rel wrel 4773   Fun wfun 5328
This theorem is referenced by:  funeu  5357  nfunv  5364  funopg  5365  funssres  5373  funun  5375  fununi  5395  funcnvres2  5402  fnrel  5421  fcoi1  5495  f1orel  5555  funbrfv  5641  funbrfv2b  5647  funfv2  5667  funfvbrb  5718  fmptco  5771  tfrlem6  6482  tfr2b  6496  pmresg  6880  fundmen  7019  rankwflemb  7552  gruima  8511  structcnvcnv  13250  inviso1  13761  setciso  14016  00lsp  15831  fimacnvinrn  23248  fmptcof2  23277  fundmpss  24680  funsseq  24683  wfrlem6  24819  frrlem5b  24844  frrlem6  24848  nofulllem3  24916  nofulllem5  24918  dffun10  25011  imageval  25027  cocnv  25717  funbrafv  27346  funbrafv2b  27347  constr3pthlem1  27762  bnj1379  28608
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-fun 5336
  Copyright terms: Public domain W3C validator