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

Theorem relcnv 5169
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 4804 . 2  |-  `' A  =  { <. x ,  y
>.  |  y A x }
21relopabi 4921 1  |-  Rel  `' A
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4366   `'ccnv 4795   Rel wrel 4801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-opab 4426  df-xp 4802  df-rel 4803  df-cnv 4804
This theorem is referenced by:  relbrcnvg  5170  eliniseg2  5171  cnvsym  5176  intasym  5177  asymref  5178  cnvopab  5199  cnv0  5201  cnvdif  5204  dfrel2  5248  cnvcnv  5250  cnvsn0  5266  cnvcnvsn  5275  resdm2  5287  coi2  5314  coires1  5315  cnvssrndm  5319  unidmrn  5328  cnviin  5335  predep  5368  funi  5574  funcnvsn  5589  funcnv2  5603  fcnvres  5720  f1cnvcnv  5747  f1ompt  6003  fliftcnv  6163  cnvexg  6697  cnvf1o  6850  fsplit  6856  reldmtpos  6936  dmtpos  6940  rntpos  6941  dftpos3  6946  dftpos4  6947  tpostpos  6948  tposf12  6953  ercnv  7339  omxpenlem  7626  domss2  7684  cnvfi  7809  trclublem  13003  relexpaddg  13060  fsumcnv  13777  fsumcom2  13778  fprodcnv  13980  fprodcom2  13981  invsym2  15611  oppcsect2  15627  cnvps  16401  tsrdir  16427  mvdco  17029  gsumcom2  17550  funcnvmptOLD  28216  funcnvmpt  28217  fcnvgreu  28221  dfcnv2  28225  cnvct  28249  gsummpt2co  28494  cnvco1  30351  cnvco2  30352  colinrel  30773  trer  30921  cnvnonrel  36107  cnvcnvintabd  36119  cnvintabd  36122  cnvssco  36125  clrellem  36142  clcnvlem  36143  cnviun  36155  trrelsuperrel2dg  36176  dffrege115  36487
  Copyright terms: Public domain W3C validator