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

Theorem relcnv 5226
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 4861 . 2  |-  `' A  =  { <. x ,  y
>.  |  y A x }
21relopabi 4978 1  |-  Rel  `' A
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4416   `'ccnv 4852   Rel wrel 4858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-opab 4476  df-xp 4859  df-rel 4860  df-cnv 4861
This theorem is referenced by:  relbrcnvg  5227  eliniseg2  5228  cnvsym  5233  intasym  5234  asymref  5235  cnvopab  5256  cnv0  5258  cnvdif  5261  dfrel2  5305  cnvcnv  5307  cnvsn0  5323  cnvcnvsn  5332  resdm2  5344  coi2  5371  coires1  5372  cnvssrndm  5376  unidmrn  5385  cnviin  5392  predep  5425  funi  5631  funcnvsn  5646  funcnv2  5664  fcnvres  5783  f1cnvcnv  5810  f1ompt  6067  fliftcnv  6229  cnvexg  6766  cnvf1o  6922  fsplit  6928  reldmtpos  7007  dmtpos  7011  rntpos  7012  dftpos3  7017  dftpos4  7018  tpostpos  7019  tposf12  7024  ercnv  7410  omxpenlem  7699  domss2  7757  cnvfi  7882  trclublem  13108  relexpaddg  13165  fsumcnv  13883  fsumcom2  13884  fprodcnv  14086  fprodcom2  14087  invsym2  15717  oppcsect2  15733  cnvps  16507  tsrdir  16533  mvdco  17135  gsumcom2  17656  funcnvmptOLD  28319  funcnvmpt  28320  fcnvgreu  28324  dfcnv2  28328  cnvct  28348  gsummpt2co  28592  cnvco1  30449  cnvco2  30450  colinrel  30873  trer  31021  cnvnonrel  36239  cnvcnvintabd  36251  cnvintabd  36254  cnvssco  36257  clrellem  36274  clcnvlem  36275  cnviun  36287  trrelsuperrel2dg  36308  dffrege115  36619
  Copyright terms: Public domain W3C validator