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

Theorem funrel 5438
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 5423 . 2  |-  ( Fun 
A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
21simplbi 447 1  |-  ( Fun 
A  ->  Rel  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3288    _I cid 4461   `'ccnv 4844    o. ccom 4849   Rel wrel 4850   Fun wfun 5415
This theorem is referenced by:  funeu  5444  nfunv  5451  funopg  5452  funssres  5460  funun  5462  fununi  5484  funcnvres2  5491  fnrel  5510  fcoi1  5584  f1orel  5644  funbrfv  5732  funbrfv2b  5738  funfv2  5758  funfvbrb  5810  fmptco  5868  tfrlem6  6610  tfr2b  6624  pmresg  7008  fundmen  7147  rankwflemb  7683  gruima  8641  structcnvcnv  13443  inviso1  13954  setciso  14209  00lsp  16020  constr3pthlem1  21603  fimacnvinrn  24008  fmptcof2  24037  fundmpss  25344  funsseq  25347  wfrlem6  25483  frrlem5b  25508  frrlem6  25512  nofulllem3  25580  nofulllem5  25582  dffun10  25675  imageval  25691  cocnv  26325  funbrafv  27897  funbrafv2b  27898  bnj1379  28920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-fun 5423
  Copyright terms: Public domain W3C validator