Theorem relcnv 6073

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.

Step	Hyp	Ref	Expression
1		df-cnv 5642	. 2 ⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
2	1	relopabiv 5779	1 ⊢ Rel ◡𝐴

Syntax hints:   class class class wbr 5100  ^◡ccnv 5633  Rel wrel 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-opab 5163  df-xp 5640  df-rel 5641  df-cnv 5642

This theorem is referenced by:  relbrcnvg  6074  eliniseg2  6075  cnvsym  6081  intasym  6082  asymref  6083  cnvopab  6104  cnvopabOLD  6105  cnvdif  6111  dfrel2  6157  cnvcnv  6160  cnvsn0  6178  cnvcnvsn  6187  resdm2  6199  coi2  6232  coires1  6233  cnvssrndm  6239  unidmrn  6247  cnviin  6254  predep  6298  funi  6534  funcnvsn  6552  funcnv2  6570  fcnvres  6721  f1cnvcnv  6749  funcnvmpt  6953  f1ompt  7067  fliftcnv  7269  cnvexg  7878  cnvf1o  8065  fsplit  8071  reldmtpos  8188  dmtpos  8192  rntpos  8193  dftpos3  8198  dftpos4  8199  tpostpos  8200  tposf12  8205  ercnv  8669  cnvct  8985  omxpenlem  9020  domss2  9078  cnvfi  9114  cnvfiALT  9253  trclublem  14932  relexpaddg  14990  fsumcnv  15710  fsumcom2  15711  fprodcnv  15920  fprodcom2  15921  invsym2  17701  oppcsect2  17717  cnvps  18515  tsrdir  18541  mvdco  19391  gsumcom2  19921  fcnvgreu  32768  dfcnv2  32771  gsummpt2co  33148  gsumhashmul  33167  cnvco1  35981  cnvco2  35982  colinrel  36279  trer  36538  releleccnv  38540  elec1cnvres  38555  eleccnvep  38567  brcnvrabga  38622  cnvresrn  38628  ineccnvmo  38637  elec1cnvxrn2  38700  dfsucmap3  38743  cnvelrels  38856  dfdisjALTV  39078  dfeldisj5  39093  dfantisymrel4  39144  dfantisymrel5  39145  cnvnonrel  43973  cnvcnvintabd  43985  cnvintabd  43988  cnvssco  43991  clrellem  44007  clcnvlem  44008  cnviun  44035  trrelsuperrel2dg  44056  dffrege115  44363  dmtposss  49264  tposrescnv  49267  tposres3  49269  tposideq  49276