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

Theorem relcnv 5233
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 4877 . 2  |-  `' A  =  { <. x ,  y
>.  |  y A x }
21relopabi 4991 1  |-  Rel  `' A
Colors of variables: wff set class
Syntax hints:   class class class wbr 4204   `'ccnv 4868   Rel wrel 4874
This theorem is referenced by:  relbrcnvg  5234  eliniseg2  5235  cnvsym  5239  intasym  5240  asymref  5241  cnvopab  5265  cnv0  5266  cnvdif  5269  dfrel2  5312  cnvcnv  5314  cnvsn0  5329  cnvcnvsn  5338  resdm2  5351  coi2  5377  coires1  5378  cnvssrndm  5382  unidmrn  5390  cnvexg  5396  cnviin  5400  funi  5474  funcnvsn  5487  funcnv2  5501  fcnvres  5611  f1cnvcnv  5638  f1ompt  5882  fliftcnv  6024  cnvf1o  6436  fsplit  6442  reldmtpos  6478  dmtpos  6482  rntpos  6483  dftpos3  6488  dftpos4  6489  tpostpos  6490  tposf12  6495  ercnv  6917  omxpenlem  7200  domss2  7257  cnvfi  7381  fsumcnv  12545  fsumcom2  12546  invsym2  13976  oppcsect2  13988  cnvps  14632  tsrdir  14671  gsumcom2  15537  funcnvmptOLD  24070  funcnvmpt  24071  cnvct  24095  relexpcnv  25121  relexprel  25122  fprodcnv  25296  fprodcom2  25297  cnvco1  25372  cnvco2  25373  predep  25447  colinrel  25939  trer  26256  mvdco  27303
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-opab 4259  df-xp 4875  df-rel 4876  df-cnv 4877
  Copyright terms: Public domain W3C validator