Theorem relcnv 6107

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

Syntax hints:   class class class wbr 5111  ^◡ccnv 5661  Rel wrel 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3463  df-ss 3928  df-opab 5176  df-xp 5668  df-rel 5669  df-cnv 5670

This theorem is referenced by:  relbrcnvg  6108  eliniseg2  6109  cnvsym  6115  intasym  6116  asymref  6117  cnvopab  6138  cnvdif  6141  dfrel2  6188  cnvcnv  6191  cnvsn0  6212  cnvcnvsn  6221  resdm2  6233  coi2  6266  coires1  6267  cnvssrndm  6273  unidmrn  6281  cnviin  6288  predep  6332  funi  6569  funcnvsn  6587  funcnv2  6605  fcnvres  6756  f1cnvcnv  6786  funcnvmpt  6992  f1ompt  7107  fliftcnv  7310  cnvexg  7921  cnvf1o  8106  fsplit  8112  reldmtpos  8230  dmtpos  8234  rntpos  8235  dftpos3  8240  dftpos4  8241  tpostpos  8242  tposf12  8247  ercnv  8716  cnvct  9031  omxpenlem  9066  domss2  9124  cnvfi  9160  cnvfiALT  9296  trclublem  15032  relexpaddg  15090  fsumcnv  15824  fsumcom2  15825  fprodcnv  16037  fprodcom2  16038  invsym2  17820  oppcsect2  17836  cnvps  18634  tsrdir  18660  mvdco  19515  gsumcom2  20045  fcnvgreu  32958  dfcnv2  32961  gsummpt2co  33309  gsumhashmul  33328  cnvco1  36184  cnvco2  36185  colinrel  36482  trer  36750  releleccnv  38834  elec1cnvres  38849  eleccnvep  38861  brcnvrabga  38916  cnvresrn  38922  ineccnvmo  38931  elec1cnvxrn2  38994  dfsucmap3  39037  cnvelrels  39150  dfdisjALTV  39372  dfeldisj5  39387  dfantisymrel4  39438  dfantisymrel5  39439  cnvnonrel  44241  cnvcnvintabd  44253  cnvintabd  44256  cnvssco  44259  clrellem  44275  clcnvlem  44276  cnviun  44303  trrelsuperrel2dg  44324  dffrege115  44631  dmtposss  49574  tposrescnv  49577  tposres3  49579  tposideq  49586