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

Theorem funrel 5561
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 5546 . 2  |-  ( Fun 
A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
21simplbi 461 1  |-  ( Fun 
A  ->  Rel  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3379    _I cid 4706   `'ccnv 4795    o. ccom 4800   Rel wrel 4801   Fun wfun 5538
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 188  df-an 372  df-fun 5546
This theorem is referenced by:  funeu  5568  nfunv  5575  funopg  5576  funssres  5584  funun  5586  fununfun  5588  fununi  5610  funcnvres2  5615  fnrel  5635  fcoi1  5717  f1orel  5777  funbrfv  5863  funbrfv2b  5869  funfv2  5893  funfvbrb  5954  fvn0ssdmfun  5972  fmptco  6015  funresdfunsn  6065  wfrrel  6996  tfrlem6  7055  tfr2b  7069  pmresg  7454  fundmen  7597  resfifsupp  7864  rankwflemb  8216  gruima  9178  structcnvcnv  15075  inviso1  15614  setciso  15929  pmtrsn  17103  00lsp  18147  constr3pthlem1  25325  0eusgraiff0rgracl  25611  fimacnvinrn  28181  fmptcof2  28205  fgreu  28220  bnj1379  29594  fundmpss  30358  funsseq  30360  frrlem5b  30470  frrlem6  30474  nofulllem3  30542  nofulllem5  30544  imageval  30646  imagesset  30669  cocnv  31959  frege124d  36266  frege129d  36268  frege133d  36270  funbrafv  38473  funbrafv2b  38474  funopsn  38825  uhgriedg0edg0  39068  edg0usgr  39078  usgr1v0edg  39081  egrsubgr  39096  rngciso  39585  rngcisoALTV  39597  ringciso  39636  ringcisoALTV  39660
  Copyright terms: Public domain W3C validator