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

Theorem funrel 5587
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 5572 . 2  |-  ( Fun 
A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
21simplbi 458 1  |-  ( Fun 
A  ->  Rel  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3461    _I cid 4779   `'ccnv 4987    o. ccom 4992   Rel wrel 4993   Fun wfun 5564
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 369  df-fun 5572
This theorem is referenced by:  funeu  5594  nfunv  5601  funopg  5602  funssres  5610  funun  5612  fununfun  5614  fununi  5636  funcnvres2  5641  fnrel  5661  fcoi1  5741  f1orel  5801  funbrfv  5886  funbrfv2b  5892  funfv2  5916  funfvbrb  5976  fvn0ssdmfun  5998  fmptco  6040  funresdfunsn  6089  tfrlem6  7043  tfr2b  7057  pmresg  7439  fundmen  7582  resfifsupp  7849  rankwflemb  8202  gruima  9169  structcnvcnv  14727  inviso1  15254  setciso  15569  pmtrsn  16743  00lsp  17822  constr3pthlem1  24857  0eusgraiff0rgracl  25143  fimacnvinrn  27696  fmptcof2  27724  fgreu  27740  fundmpss  29437  funsseq  29439  wfrlem6  29588  frrlem5b  29632  frrlem6  29636  nofulllem3  29704  nofulllem5  29706  imageval  29808  imagesset  29831  cocnv  30456  funbrafv  32482  funbrafv2b  32483  rngciso  33044  rngcisoALTV  33056  ringciso  33095  ringcisoALTV  33119  bnj1379  34290
  Copyright terms: Public domain W3C validator