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

Theorem funrel 5618
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 5603 . 2  |-  ( Fun 
A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
21simplbi 466 1  |-  ( Fun 
A  ->  Rel  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3416    _I cid 4763   `'ccnv 4852    o. ccom 4857   Rel wrel 4858   Fun wfun 5595
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 190  df-an 377  df-fun 5603
This theorem is referenced by:  funeu  5625  nfunv  5632  funopg  5633  funssres  5641  funun  5643  fununfun  5645  fununi  5671  funcnvres2  5676  fnrel  5696  fcoi1  5780  f1orel  5840  funbrfv  5926  funbrfv2b  5932  funfv2  5956  funfvbrb  6018  fvn0ssdmfun  6036  fmptco  6080  funresdfunsn  6130  wfrrel  7067  tfrlem6  7126  tfr2b  7140  pmresg  7525  fundmen  7669  resfifsupp  7937  rankwflemb  8290  gruima  9253  structcnvcnv  15181  inviso1  15720  setciso  16035  pmtrsn  17209  00lsp  18253  constr3pthlem1  25432  0eusgraiff0rgracl  25718  fimacnvinrn  28284  fmptcof2  28308  fgreu  28323  bnj1379  29691  fundmpss  30456  funsseq  30458  frrlem5b  30568  frrlem6  30572  nofulllem3  30642  nofulllem5  30644  imageval  30746  imagesset  30769  cocnv  32097  frege124d  36398  frege129d  36400  frege133d  36402  funbrafv  38698  funbrafv2b  38699  funopsn  39060  edg0iedg0  39266  edg0usgr  39378  usgr1v0edg  39381  rngciso  40257  rngcisoALTV  40269  ringciso  40308  ringcisoALTV  40332
  Copyright terms: Public domain W3C validator