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

Theorem relcnv 5287
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 4921 . 2  |-  `' A  =  { <. x ,  y
>.  |  y A x }
21relopabi 5040 1  |-  Rel  `' A
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4367   `'ccnv 4912   Rel wrel 4918
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-opab 4426  df-xp 4919  df-rel 4920  df-cnv 4921
This theorem is referenced by:  relbrcnvg  5288  eliniseg2  5289  cnvsym  5294  intasym  5295  asymref  5296  cnvopab  5317  cnv0  5319  cnvdif  5322  dfrel2  5366  cnvcnv  5368  cnvsn0  5384  cnvcnvsn  5393  resdm2  5405  coi2  5432  coires1  5433  cnvssrndm  5437  unidmrn  5446  cnviin  5453  funi  5526  funcnvsn  5541  funcnv2  5555  fcnvres  5670  f1cnvcnv  5697  f1ompt  5955  fliftcnv  6110  cnvexg  6645  cnvf1o  6798  fsplit  6804  reldmtpos  6881  dmtpos  6885  rntpos  6886  dftpos3  6891  dftpos4  6892  tpostpos  6893  tposf12  6898  ercnv  7250  omxpenlem  7537  domss2  7595  cnvfi  7719  trclublem  12833  relexpaddg  12888  fsumcnv  13590  fsumcom2  13591  fprodcnv  13789  fprodcom2  13790  invsym2  15169  oppcsect2  15185  cnvps  15959  tsrdir  15985  mvdco  16587  gsumcom2  17117  funcnvmptOLD  27655  funcnvmpt  27656  fcnvgreu  27660  dfcnv2  27664  cnvct  27687  gsummpt2co  27924  cnvco1  29355  cnvco2  29356  predep  29437  colinrel  29860  trer  30300  cnviun  38190  dffrege115  38477
  Copyright terms: Public domain W3C validator