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

Theorem relcnv 5685
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 5285 . 2 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
21relopabi 5414 1 Rel 𝐴
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4809  ccnv 5276  Rel wrel 5282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-opab 4872  df-xp 5283  df-rel 5284  df-cnv 5285
This theorem is referenced by:  relbrcnvg  5686  eliniseg2  5687  cnvsym  5693  intasym  5694  asymref  5695  cnvopab  5716  cnv0OLD  5719  cnvdif  5722  dfrel2  5766  cnvcnv  5769  cnvcnvOLD  5770  cnvsn0  5786  cnvcnvsn  5796  resdm2  5810  coi2  5838  coires1  5839  cnvssrndm  5843  unidmrn  5851  cnviin  5858  predep  5891  funi  6100  funcnvsn  6117  funcnv2  6135  fcnvres  6264  f1cnvcnv  6292  f1ompt  6571  fliftcnv  6753  cnvexg  7310  cnvf1o  7478  fsplit  7484  reldmtpos  7563  dmtpos  7567  rntpos  7568  dftpos3  7573  dftpos4  7574  tpostpos  7575  tposf12  7580  ercnv  7968  cnvct  8237  omxpenlem  8268  domss2  8326  cnvfi  8455  trclublem  14021  relexpaddg  14078  fsumcnv  14789  fsumcom2  14790  fprodcnv  14996  fprodcom2  14997  invsym2  16688  oppcsect2  16704  cnvps  17478  tsrdir  17504  mvdco  18128  gsumcom2  18640  funcnvmpt  29917  fcnvgreu  29921  dfcnv2  29925  gsummpt2co  30227  cnvco1  32094  cnvco2  32095  colinrel  32608  trer  32754  releleccnv  34456  eleccnvep  34478  brcnvrabga  34539  cnvresrn  34545  ineccnvmo  34551  elec1cnvxrn2  34584  cnvelrels  34674  cnvnonrel  38569  cnvcnvintabd  38581  cnvintabd  38584  cnvssco  38587  clrellem  38604  clcnvlem  38605  cnviun  38617  trrelsuperrel2dg  38638  dffrege115  38946
  Copyright terms: Public domain W3C validator