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

Theorem relcnv 5227
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 4862 . 2  |-  `' A  =  { <. x ,  y
>.  |  y A x }
21relopabi 4979 1  |-  Rel  `' A
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4426   `'ccnv 4853   Rel wrel 4859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-opab 4485  df-xp 4860  df-rel 4861  df-cnv 4862
This theorem is referenced by:  relbrcnvg  5228  eliniseg2  5229  cnvsym  5234  intasym  5235  asymref  5236  cnvopab  5257  cnv0  5259  cnvdif  5262  dfrel2  5306  cnvcnv  5308  cnvsn0  5324  cnvcnvsn  5333  resdm2  5345  coi2  5372  coires1  5373  cnvssrndm  5377  unidmrn  5386  cnviin  5393  predep  5425  funi  5631  funcnvsn  5646  funcnv2  5660  fcnvres  5777  f1cnvcnv  5804  f1ompt  6059  fliftcnv  6219  cnvexg  6753  cnvf1o  6906  fsplit  6912  reldmtpos  6989  dmtpos  6993  rntpos  6994  dftpos3  6999  dftpos4  7000  tpostpos  7001  tposf12  7006  ercnv  7392  omxpenlem  7679  domss2  7737  cnvfi  7862  trclublem  13038  relexpaddg  13095  fsumcnv  13812  fsumcom2  13813  fprodcnv  14015  fprodcom2  14016  invsym2  15619  oppcsect2  15635  cnvps  16409  tsrdir  16435  mvdco  17037  gsumcom2  17542  funcnvmptOLD  28110  funcnvmpt  28111  fcnvgreu  28115  dfcnv2  28119  cnvct  28142  gsummpt2co  28381  cnvco1  30187  cnvco2  30188  colinrel  30609  trer  30757  cnviun  35880  trrelsuperrel2dg  35901  dffrege115  36210
  Copyright terms: Public domain W3C validator