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

Theorem funrel 5272
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 5257 . 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 3152    _I cid 4304   `'ccnv 4688    o. ccom 4693   Rel wrel 4694   Fun wfun 5249
This theorem is referenced by:  funeu  5278  nfunv  5285  funopg  5286  funssres  5294  funun  5296  fununi  5316  funcnvres2  5323  fnrel  5342  fcoi1  5415  f1orel  5475  funbrfv  5561  funbrfv2b  5567  funfv2  5587  funfvbrb  5638  fmptco  5691  tfrlem6  6398  tfr2b  6412  pmresg  6795  fundmen  6934  rankwflemb  7465  gruima  8424  structcnvcnv  13159  inviso1  13668  setciso  13923  00lsp  15738  fimacnvinrn  23199  fmptcof2  23229  fundmpss  24122  funsseq  24125  wfrlem6  24261  frrlem5b  24286  frrlem6  24290  nofulllem3  24358  nofulllem5  24360  dffun10  24453  imageval  24469  cocnv  26393  funbrafv  28020  funbrafv2b  28021  bnj1379  28863
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 5257
  Copyright terms: Public domain W3C validator