Theorem relcnv 6067

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

Syntax hints:   class class class wbr 5086  ^◡ccnv 5627  Rel wrel 5633

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 3432  df-ss 3907  df-opab 5149  df-xp 5634  df-rel 5635  df-cnv 5636

This theorem is referenced by:  relbrcnvg  6068  eliniseg2  6069  cnvsym  6075  intasym  6076  asymref  6077  cnvopab  6098  cnvopabOLD  6099  cnvdif  6105  dfrel2  6151  cnvcnv  6154  cnvsn0  6172  cnvcnvsn  6181  resdm2  6193  coi2  6226  coires1  6227  cnvssrndm  6233  unidmrn  6241  cnviin  6248  predep  6292  funi  6528  funcnvsn  6546  funcnv2  6564  fcnvres  6715  f1cnvcnv  6743  funcnvmpt  6947  f1ompt  7061  fliftcnv  7263  cnvexg  7872  cnvf1o  8058  fsplit  8064  reldmtpos  8181  dmtpos  8185  rntpos  8186  dftpos3  8191  dftpos4  8192  tpostpos  8193  tposf12  8198  ercnv  8662  cnvct  8978  omxpenlem  9013  domss2  9071  cnvfi  9107  cnvfiALT  9246  trclublem  14954  relexpaddg  15012  fsumcnv  15732  fsumcom2  15733  fprodcnv  15945  fprodcom2  15946  invsym2  17727  oppcsect2  17743  cnvps  18541  tsrdir  18567  mvdco  19417  gsumcom2  19947  fcnvgreu  32766  dfcnv2  32769  gsummpt2co  33130  gsumhashmul  33149  cnvco1  35963  cnvco2  35964  colinrel  36261  trer  36520  releleccnv  38603  elec1cnvres  38618  eleccnvep  38630  brcnvrabga  38685  cnvresrn  38691  ineccnvmo  38700  elec1cnvxrn2  38763  dfsucmap3  38806  cnvelrels  38919  dfdisjALTV  39141  dfeldisj5  39156  dfantisymrel4  39207  dfantisymrel5  39208  cnvnonrel  44041  cnvcnvintabd  44053  cnvintabd  44056  cnvssco  44059  clrellem  44075  clcnvlem  44076  cnviun  44103  trrelsuperrel2dg  44124  dffrege115  44431  dmtposss  49371  tposrescnv  49374  tposres3  49376  tposideq  49383