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

Theorem funrel 5500
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 5485 . 2  |-  ( Fun 
A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
21simplbi 448 1  |-  ( Fun 
A  ->  Rel  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3306    _I cid 4522   `'ccnv 4906    o. ccom 4911   Rel wrel 4912   Fun wfun 5477
This theorem is referenced by:  funeu  5506  nfunv  5513  funopg  5514  funssres  5522  funun  5524  fununi  5546  funcnvres2  5553  fnrel  5572  fcoi1  5646  f1orel  5706  funbrfv  5794  funbrfv2b  5800  funfv2  5820  funfvbrb  5872  fmptco  5930  tfrlem6  6672  tfr2b  6686  pmresg  7070  fundmen  7209  rankwflemb  7748  gruima  8708  structcnvcnv  13511  inviso1  14022  setciso  14277  00lsp  16088  constr3pthlem1  21673  fimacnvinrn  24078  fmptcof2  24107  fundmpss  25421  funsseq  25424  wfrlem6  25574  frrlem5b  25618  frrlem6  25622  nofulllem3  25690  nofulllem5  25692  imageval  25806  imagesset  25829  cocnv  26465  funbrafv  28036  funbrafv2b  28037  bnj1379  29300
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 179  df-an 362  df-fun 5485
  Copyright terms: Public domain W3C validator