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

Theorem relcnv 6122
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 5693 . 2 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
21relopabiv 5830 1 Rel 𝐴
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 5143  ccnv 5684  Rel wrel 5690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693
This theorem is referenced by:  relbrcnvg  6123  eliniseg2  6124  cnvsym  6132  cnvsymOLD  6133  cnvsymOLDOLD  6134  intasym  6135  asymref  6136  cnvopab  6157  cnvopabOLD  6158  cnvdif  6163  dfrel2  6209  cnvcnv  6212  cnvsn0  6230  cnvcnvsn  6239  resdm2  6251  coi2  6283  coires1  6284  cnvssrndm  6291  unidmrn  6299  cnviin  6306  predep  6351  funi  6598  funcnvsn  6616  funcnv2  6634  fcnvres  6785  f1cnvcnv  6813  f1ompt  7131  fliftcnv  7331  cnvexg  7946  cnvf1o  8136  fsplit  8142  reldmtpos  8259  dmtpos  8263  rntpos  8264  dftpos3  8269  dftpos4  8270  tpostpos  8271  tposf12  8276  ercnv  8766  cnvct  9074  omxpenlem  9113  domss2  9176  cnvfi  9216  cnvfiALT  9379  trclublem  15034  relexpaddg  15092  fsumcnv  15809  fsumcom2  15810  fprodcnv  16019  fprodcom2  16020  invsym2  17807  oppcsect2  17823  cnvps  18623  tsrdir  18649  mvdco  19463  gsumcom2  19993  funcnvmpt  32677  fcnvgreu  32683  dfcnv2  32686  gsummpt2co  33051  gsumhashmul  33064  cnvco1  35759  cnvco2  35760  colinrel  36058  trer  36317  releleccnv  38258  eleccnvep  38282  brcnvrabga  38343  cnvresrn  38349  ineccnvmo  38358  elec1cnvxrn2  38398  cnvelrels  38496  dfdisjALTV  38714  dfeldisj5  38722  dfantisymrel4  38762  dfantisymrel5  38763  cnvnonrel  43601  cnvcnvintabd  43613  cnvintabd  43616  cnvssco  43619  clrellem  43635  clcnvlem  43636  cnviun  43663  trrelsuperrel2dg  43684  dffrege115  43991  dmtposss  48776  tposrescnv  48779  tposres3  48781  tposideq  48788
  Copyright terms: Public domain W3C validator