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

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

Proof of Theorem relcnv
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-cnv 5531 . 2 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
21relopabi 5662 1 Rel 𝐴
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 5033  ccnv 5522  Rel wrel 5528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-opab 5096  df-xp 5529  df-rel 5530  df-cnv 5531
This theorem is referenced by:  relbrcnvg  5939  eliniseg2  5940  cnvsym  5945  intasym  5946  asymref  5947  cnvopab  5968  cnvdif  5973  dfrel2  6017  cnvcnv  6020  cnvsn0  6038  cnvcnvsn  6047  resdm2  6059  coi2  6087  coires1  6088  cnvssrndm  6094  unidmrn  6102  cnviin  6109  predep  6146  funi  6360  funcnvsn  6378  funcnv2  6396  fcnvres  6534  f1cnvcnv  6563  f1ompt  6856  fliftcnv  7047  cnvexg  7615  cnvf1o  7793  fsplit  7799  fsplitOLD  7800  reldmtpos  7887  dmtpos  7891  rntpos  7892  dftpos3  7897  dftpos4  7898  tpostpos  7899  tposf12  7904  ercnv  8297  cnvct  8573  omxpenlem  8605  domss2  8664  cnvfi  8794  trclublem  14350  relexpaddg  14407  fsumcnv  15123  fsumcom2  15124  fprodcnv  15332  fprodcom2  15333  invsym2  17028  oppcsect2  17044  cnvps  17817  tsrdir  17843  mvdco  18568  gsumcom2  19091  funcnvmpt  30433  fcnvgreu  30439  dfcnv2  30442  gsummpt2co  30736  gsumhashmul  30744  cnvco1  33103  cnvco2  33104  colinrel  33626  trer  33772  releleccnv  35671  eleccnvep  35691  brcnvrabga  35752  cnvresrn  35758  ineccnvmo  35764  elec1cnvxrn2  35798  cnvelrels  35888  dfdisjALTV  36099  dfeldisj5  36107  cnvnonrel  40275  cnvcnvintabd  40287  cnvintabd  40290  cnvssco  40293  clrellem  40309  clcnvlem  40310  cnviun  40338  trrelsuperrel2dg  40359  dffrege115  40666
  Copyright terms: Public domain W3C validator