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

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

Proof of Theorem relcnv
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-cnv 5012 . 2
21relopabi 5133 1
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4452  `'ccnv 5003  Relwrel 5009
This theorem is referenced by:  relbrcnvg  5380  eliniseg2  5381  cnvsym  5386  intasym  5387  asymref  5388  cnvopab  5412  cnv0  5414  cnvdif  5417  dfrel2  5462  cnvcnv  5464  cnvsn0  5481  cnvcnvsn  5490  resdm2  5502  coi2  5529  coires1  5530  cnvssrndm  5534  unidmrn  5542  cnviin  5549  funi  5623  funcnvsn  5638  funcnv2  5652  fcnvres  5767  f1cnvcnv  5794  f1ompt  6053  fliftcnv  6209  cnvexg  6746  cnvf1o  6899  fsplit  6905  reldmtpos  6982  dmtpos  6986  rntpos  6987  dftpos3  6992  dftpos4  6993  tpostpos  6994  tposf12  6999  ercnv  7351  omxpenlem  7638  domss2  7696  cnvfi  7824  fsumcnv  13588  fsumcom2  13589  fprodcnv  13787  fprodcom2  13788  invsym2  15157  oppcsect2  15169  cnvps  15842  tsrdir  15868  mvdco  16470  gsumcom2  17003  funcnvmptOLD  27509  funcnvmpt  27510  fcnvgreu  27514  dfcnv2  27517  cnvct  27538  gsummpt2co  27771  relexpcnv  29056  relexprel  29057  cnvco1  29189  cnvco2  29190  predep  29272  colinrel  29707  trer  30134  trclubg  37785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-opab 4511  df-xp 5010  df-rel 5011  df-cnv 5012
  Copyright terms: Public domain W3C validator