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

Theorem relcnv 6060
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 5645 . 2 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
21relopabiv 5780 1 Rel 𝐴
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 5109  ccnv 5636  Rel wrel 5642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3449  df-in 3921  df-ss 3931  df-opab 5172  df-xp 5643  df-rel 5644  df-cnv 5645
This theorem is referenced by:  relbrcnvg  6061  eliniseg2  6062  cnvsym  6070  cnvsymOLD  6071  cnvsymOLDOLD  6072  intasym  6073  asymref  6074  cnvopab  6095  cnvdif  6100  dfrel2  6145  cnvcnv  6148  cnvsn0  6166  cnvcnvsn  6175  resdm2  6187  coi2  6219  coires1  6220  cnvssrndm  6227  unidmrn  6235  cnviin  6242  predep  6288  funi  6537  funcnvsn  6555  funcnv2  6573  fcnvres  6723  f1cnvcnv  6752  f1ompt  7063  fliftcnv  7260  cnvexg  7865  cnvf1o  8047  fsplit  8053  reldmtpos  8169  dmtpos  8173  rntpos  8174  dftpos3  8179  dftpos4  8180  tpostpos  8181  tposf12  8186  ercnv  8675  cnvct  8984  omxpenlem  9023  domss2  9086  cnvfi  9130  cnvfiALT  9284  trclublem  14889  relexpaddg  14947  fsumcnv  15666  fsumcom2  15667  fprodcnv  15874  fprodcom2  15875  invsym2  17654  oppcsect2  17670  cnvps  18475  tsrdir  18501  mvdco  19235  gsumcom2  19760  funcnvmpt  31636  fcnvgreu  31642  dfcnv2  31645  gsummpt2co  31946  gsumhashmul  31954  cnvco1  34395  cnvco2  34396  colinrel  34695  trer  34841  releleccnv  36767  eleccnvep  36791  brcnvrabga  36853  cnvresrn  36859  ineccnvmo  36868  elec1cnvxrn2  36909  cnvelrels  37007  dfdisjALTV  37225  dfeldisj5  37233  dfantisymrel4  37273  dfantisymrel5  37274  cnvnonrel  41952  cnvcnvintabd  41964  cnvintabd  41967  cnvssco  41970  clrellem  41986  clcnvlem  41987  cnviun  42014  trrelsuperrel2dg  42035  dffrege115  42342
  Copyright terms: Public domain W3C validator