Theorem relcnv 6052

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 5622	. 2 ⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
2	1	relopabiv 5759	1 ⊢ Rel ◡𝐴

Syntax hints:   class class class wbr 5089  ^◡ccnv 5613  Rel wrel 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-opab 5152  df-xp 5620  df-rel 5621  df-cnv 5622

This theorem is referenced by:  relbrcnvg  6053  eliniseg2  6054  cnvsym  6060  intasym  6061  asymref  6062  cnvopab  6083  cnvopabOLD  6084  cnvdif  6090  dfrel2  6136  cnvcnv  6139  cnvsn0  6157  cnvcnvsn  6166  resdm2  6178  coi2  6211  coires1  6212  cnvssrndm  6218  unidmrn  6226  cnviin  6233  predep  6277  funi  6513  funcnvsn  6531  funcnv2  6549  fcnvres  6700  f1cnvcnv  6728  f1ompt  7044  fliftcnv  7245  cnvexg  7854  cnvf1o  8041  fsplit  8047  reldmtpos  8164  dmtpos  8168  rntpos  8169  dftpos3  8174  dftpos4  8175  tpostpos  8176  tposf12  8181  ercnv  8643  cnvct  8956  omxpenlem  8991  domss2  9049  cnvfi  9085  cnvfiALT  9223  trclublem  14902  relexpaddg  14960  fsumcnv  15680  fsumcom2  15681  fprodcnv  15890  fprodcom2  15891  invsym2  17670  oppcsect2  17686  cnvps  18484  tsrdir  18510  mvdco  19357  gsumcom2  19887  funcnvmpt  32649  fcnvgreu  32655  dfcnv2  32658  gsummpt2co  33028  gsumhashmul  33041  cnvco1  35803  cnvco2  35804  colinrel  36101  trer  36360  releleccnv  38293  elec1cnvres  38306  eleccnvep  38318  brcnvrabga  38373  cnvresrn  38379  ineccnvmo  38388  elec1cnvxrn2  38443  dfsucmap3  38475  cnvelrels  38587  dfdisjALTV  38810  dfeldisj5  38818  dfantisymrel4  38858  dfantisymrel5  38859  cnvnonrel  43680  cnvcnvintabd  43692  cnvintabd  43695  cnvssco  43698  clrellem  43714  clcnvlem  43715  cnviun  43742  trrelsuperrel2dg  43763  dffrege115  44070  dmtposss  48975  tposrescnv  48978  tposres3  48980  tposideq  48987