Theorem relcnv 6064

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 5774	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  6065  eliniseg2  6066  cnvsym  6073  cnvsymOLD  6074  cnvsymOLDOLD  6075  intasym  6076  asymref  6077  cnvopab  6098  cnvopabOLD  6099  cnvdif  6104  dfrel2  6150  cnvcnv  6153  cnvsn0  6171  cnvcnvsn  6180  resdm2  6192  coi2  6224  coires1  6225  cnvssrndm  6232  unidmrn  6240  cnviin  6247  predep  6291  funi  6532  funcnvsn  6550  funcnv2  6568  fcnvres  6719  f1cnvcnv  6747  f1ompt  7065  fliftcnv  7268  cnvexg  7880  cnvf1o  8067  fsplit  8073  reldmtpos  8190  dmtpos  8194  rntpos  8195  dftpos3  8200  dftpos4  8201  tpostpos  8202  tposf12  8207  ercnv  8669  cnvct  8982  omxpenlem  9019  domss2  9077  cnvfi  9117  cnvfiALT  9266  trclublem  14938  relexpaddg  14996  fsumcnv  15716  fsumcom2  15717  fprodcnv  15926  fprodcom2  15927  invsym2  17706  oppcsect2  17722  cnvps  18520  tsrdir  18546  mvdco  19360  gsumcom2  19890  funcnvmpt  32642  fcnvgreu  32648  dfcnv2  32651  gsummpt2co  33032  gsumhashmul  33045  cnvco1  35740  cnvco2  35741  colinrel  36039  trer  36298  releleccnv  38240  eleccnvep  38263  brcnvrabga  38318  cnvresrn  38324  ineccnvmo  38333  elec1cnvxrn2  38377  cnvelrels  38480  dfdisjALTV  38699  dfeldisj5  38707  dfantisymrel4  38747  dfantisymrel5  38748  cnvnonrel  43571  cnvcnvintabd  43583  cnvintabd  43586  cnvssco  43589  clrellem  43605  clcnvlem  43606  cnviun  43633  trrelsuperrel2dg  43654  dffrege115  43961  dmtposss  48858  tposrescnv  48861  tposres3  48863  tposideq  48870