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

Theorem funrel 5535
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 5520 . 2  |-  ( Fun 
A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
21simplbi 460 1  |-  ( Fun 
A  ->  Rel  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3428    _I cid 4731   `'ccnv 4939    o. ccom 4944   Rel wrel 4945   Fun wfun 5512
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 371  df-fun 5520
This theorem is referenced by:  funeu  5542  nfunv  5549  funopg  5550  funssres  5558  funun  5560  fununfun  5562  fununi  5584  funcnvres2  5589  fnrel  5609  fcoi1  5685  f1orel  5744  funbrfv  5831  funbrfv2b  5837  funfv2  5860  funfvbrb  5917  fmptco  5977  funresdfunsn  6021  tfrlem6  6943  tfr2b  6957  pmresg  7342  fundmen  7485  rankwflemb  8103  gruima  9072  structcnvcnv  14289  inviso1  14808  setciso  15063  pmtrsn  16129  00lsp  17170  constr3pthlem1  23678  fimacnvinrn  26088  fmptcof2  26115  fgreu  26126  fundmpss  27713  funsseq  27716  wfrlem6  27865  frrlem5b  27909  frrlem6  27913  nofulllem3  27981  nofulllem5  27983  imageval  28097  imagesset  28120  cocnv  28759  funbrafv  30204  funbrafv2b  30205  bnj1379  32126
  Copyright terms: Public domain W3C validator