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

Theorem relcnv 5067
Description: A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed by NM, 29-Oct-1996.)
Assertion
Ref Expression
relcnv  |-  Rel  `' A

Proof of Theorem relcnv
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-cnv 4713 . 2  |-  `' A  =  { <. x ,  y
>.  |  y A x }
21relopabi 4827 1  |-  Rel  `' A
Colors of variables: wff set class
Syntax hints:   class class class wbr 4039   `'ccnv 4704   Rel wrel 4710
This theorem is referenced by:  relbrcnvg  5068  eliniseg2  5069  cnvsym  5073  intasym  5074  asymref  5075  cnvopab  5099  cnv0  5100  cnvdif  5103  dfrel2  5140  cnvcnv  5142  cnvsn0  5157  cnvcnvsn  5166  resdm2  5179  coi2  5205  coires1  5206  cnvssrndm  5210  unidmrn  5218  cnvexg  5224  cnviin  5228  funi  5300  funcnvsn  5313  funcnv2  5325  fcnvres  5434  f1cnvcnv  5461  f1ompt  5698  fliftcnv  5826  cnvf1o  6233  fsplit  6239  reldmtpos  6258  dmtpos  6262  rntpos  6263  dftpos3  6268  dftpos4  6269  tpostpos  6270  tposf12  6275  ercnv  6697  omxpenlem  6979  domss2  7036  cnvfi  7156  fsumcnv  12252  fsumcom2  12253  invsym2  13681  oppcsect2  13693  cnvps  14337  tsrdir  14376  gsumcom2  15242  funcnvmptOLD  23249  funcnvmpt  23250  cnvct  23358  relexpcnv  24044  relexprel  24046  cnvco1  24188  cnvco2  24189  predep  24263  colinrel  24752  cnvref2  25169  dupre1  25346  trer  26330  mvdco  27491
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-opab 4094  df-xp 4711  df-rel 4712  df-cnv 4713
  Copyright terms: Public domain W3C validator