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

Theorem relcnv 5211
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 4853 . 2  |-  `' A  =  { <. x ,  y
>.  |  y A x }
21relopabi 4970 1  |-  Rel  `' A
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4297   `'ccnv 4844   Rel wrel 4850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pr 4536
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-opab 4356  df-xp 4851  df-rel 4852  df-cnv 4853
This theorem is referenced by:  relbrcnvg  5212  eliniseg2  5213  cnvsym  5217  intasym  5218  asymref  5219  cnvopab  5243  cnv0  5245  cnvdif  5248  dfrel2  5293  cnvcnv  5295  cnvsn0  5312  cnvcnvsn  5321  resdm2  5333  coi2  5359  coires1  5360  cnvssrndm  5364  unidmrn  5372  cnviin  5379  funi  5453  funcnvsn  5468  funcnv2  5482  fcnvres  5593  f1cnvcnv  5619  f1ompt  5870  fliftcnv  6009  cnvexg  6529  cnvf1o  6676  fsplit  6682  reldmtpos  6758  dmtpos  6762  rntpos  6763  dftpos3  6768  dftpos4  6769  tpostpos  6770  tposf12  6775  ercnv  7127  omxpenlem  7417  domss2  7475  cnvfi  7600  fsumcnv  13245  fsumcom2  13246  invsym2  14706  oppcsect2  14718  cnvps  15387  tsrdir  15413  mvdco  15956  gsumcom2  16472  funcnvmptOLD  25991  funcnvmpt  25992  fcnvgreu  25996  dfcnv2  25999  cnvct  26020  gsummpt2co  26254  relexpcnv  27340  relexprel  27341  fprodcnv  27499  fprodcom2  27500  cnvco1  27575  cnvco2  27576  predep  27658  colinrel  28093  trer  28516
  Copyright terms: Public domain W3C validator