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

Theorem funrel 5603
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 5588 . 2  |-  ( Fun 
A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
21simplbi 460 1  |-  ( Fun 
A  ->  Rel  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3476    _I cid 4790   `'ccnv 4998    o. ccom 5003   Rel wrel 5004   Fun wfun 5580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-fun 5588
This theorem is referenced by:  funeu  5610  nfunv  5617  funopg  5618  funssres  5626  funun  5628  fununfun  5630  fununi  5652  funcnvres2  5657  fnrel  5677  fcoi1  5757  f1orel  5817  funbrfv  5904  funbrfv2b  5910  funfv2  5933  funfvbrb  5992  fmptco  6052  funresdfunsn  6101  tfrlem6  7048  tfr2b  7062  pmresg  7443  fundmen  7586  resfifsupp  7853  rankwflemb  8207  gruima  9176  structcnvcnv  14497  inviso1  15017  setciso  15272  pmtrsn  16340  00lsp  17410  constr3pthlem1  24331  0eusgraiff0rgracl  24617  fimacnvinrn  27148  fmptcof2  27174  fgreu  27185  fundmpss  28773  funsseq  28776  wfrlem6  28925  frrlem5b  28969  frrlem6  28973  nofulllem3  29041  nofulllem5  29043  imageval  29157  imagesset  29180  cocnv  29819  funbrafv  31710  funbrafv2b  31711  bnj1379  32968
  Copyright terms: Public domain W3C validator