Theorem relcnv 6062

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

Syntax hints:   class class class wbr 5097  ^◡ccnv 5622  Rel wrel 5628

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-ss 3917  df-opab 5160  df-xp 5629  df-rel 5630  df-cnv 5631

This theorem is referenced by:  relbrcnvg  6063  eliniseg2  6064  cnvsym  6070  intasym  6071  asymref  6072  cnvopab  6093  cnvopabOLD  6094  cnvdif  6100  dfrel2  6146  cnvcnv  6149  cnvsn0  6167  cnvcnvsn  6176  resdm2  6188  coi2  6221  coires1  6222  cnvssrndm  6228  unidmrn  6236  cnviin  6243  predep  6287  funi  6523  funcnvsn  6541  funcnv2  6559  fcnvres  6710  f1cnvcnv  6738  funcnvmpt  6942  f1ompt  7056  fliftcnv  7257  cnvexg  7866  cnvf1o  8053  fsplit  8059  reldmtpos  8176  dmtpos  8180  rntpos  8181  dftpos3  8186  dftpos4  8187  tpostpos  8188  tposf12  8193  ercnv  8657  cnvct  8973  omxpenlem  9008  domss2  9066  cnvfi  9102  cnvfiALT  9241  trclublem  14920  relexpaddg  14978  fsumcnv  15698  fsumcom2  15699  fprodcnv  15908  fprodcom2  15909  invsym2  17689  oppcsect2  17705  cnvps  18503  tsrdir  18529  mvdco  19376  gsumcom2  19906  fcnvgreu  32730  dfcnv2  32733  gsummpt2co  33110  gsumhashmul  33129  cnvco1  35932  cnvco2  35933  colinrel  36230  trer  36489  releleccnv  38430  elec1cnvres  38445  eleccnvep  38457  brcnvrabga  38512  cnvresrn  38518  ineccnvmo  38527  elec1cnvxrn2  38590  dfsucmap3  38633  cnvelrels  38746  dfdisjALTV  38968  dfeldisj5  38983  dfantisymrel4  39034  dfantisymrel5  39035  cnvnonrel  43866  cnvcnvintabd  43878  cnvintabd  43881  cnvssco  43884  clrellem  43900  clcnvlem  43901  cnviun  43928  trrelsuperrel2dg  43949  dffrege115  44256  dmtposss  49158  tposrescnv  49161  tposres3  49163  tposideq  49170