Theorem relcnv 6065

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

Syntax hints:   class class class wbr 5102  ^◡ccnv 5630  Rel wrel 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-opab 5165  df-xp 5637  df-rel 5638  df-cnv 5639

This theorem is referenced by:  relbrcnvg  6066  eliniseg2  6067  cnvsym  6074  cnvsymOLD  6075  cnvsymOLDOLD  6076  intasym  6077  asymref  6078  cnvopab  6099  cnvopabOLD  6100  cnvdif  6105  dfrel2  6151  cnvcnv  6154  cnvsn0  6172  cnvcnvsn  6181  resdm2  6193  coi2  6225  coires1  6226  cnvssrndm  6233  unidmrn  6241  cnviin  6248  predep  6292  funi  6533  funcnvsn  6551  funcnv2  6569  fcnvres  6720  f1cnvcnv  6748  f1ompt  7066  fliftcnv  7269  cnvexg  7881  cnvf1o  8068  fsplit  8074  reldmtpos  8191  dmtpos  8195  rntpos  8196  dftpos3  8201  dftpos4  8202  tpostpos  8203  tposf12  8208  ercnv  8670  cnvct  8983  omxpenlem  9020  domss2  9078  cnvfi  9118  cnvfiALT  9267  trclublem  14939  relexpaddg  14997  fsumcnv  15717  fsumcom2  15718  fprodcnv  15927  fprodcom2  15928  invsym2  17707  oppcsect2  17723  cnvps  18521  tsrdir  18547  mvdco  19361  gsumcom2  19891  funcnvmpt  32643  fcnvgreu  32649  dfcnv2  32652  gsummpt2co  33033  gsumhashmul  33046  cnvco1  35741  cnvco2  35742  colinrel  36040  trer  36299  releleccnv  38241  eleccnvep  38264  brcnvrabga  38319  cnvresrn  38325  ineccnvmo  38334  elec1cnvxrn2  38378  cnvelrels  38481  dfdisjALTV  38700  dfeldisj5  38708  dfantisymrel4  38748  dfantisymrel5  38749  cnvnonrel  43572  cnvcnvintabd  43584  cnvintabd  43587  cnvssco  43590  clrellem  43606  clcnvlem  43607  cnviun  43634  trrelsuperrel2dg  43655  dffrege115  43962  dmtposss  48859  tposrescnv  48862  tposres3  48864  tposideq  48871