Theorem relcnv 6075

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

Syntax hints:   class class class wbr 5107  ^◡ccnv 5637  Rel wrel 5643

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 3449  df-ss 3931  df-opab 5170  df-xp 5644  df-rel 5645  df-cnv 5646

This theorem is referenced by:  relbrcnvg  6076  eliniseg2  6077  cnvsym  6085  cnvsymOLD  6086  cnvsymOLDOLD  6087  intasym  6088  asymref  6089  cnvopab  6110  cnvopabOLD  6111  cnvdif  6116  dfrel2  6162  cnvcnv  6165  cnvsn0  6183  cnvcnvsn  6192  resdm2  6204  coi2  6236  coires1  6237  cnvssrndm  6244  unidmrn  6252  cnviin  6259  predep  6303  funi  6548  funcnvsn  6566  funcnv2  6584  fcnvres  6737  f1cnvcnv  6765  f1ompt  7083  fliftcnv  7286  cnvexg  7900  cnvf1o  8090  fsplit  8096  reldmtpos  8213  dmtpos  8217  rntpos  8218  dftpos3  8223  dftpos4  8224  tpostpos  8225  tposf12  8230  ercnv  8692  cnvct  9005  omxpenlem  9042  domss2  9100  cnvfi  9140  cnvfiALT  9290  trclublem  14961  relexpaddg  15019  fsumcnv  15739  fsumcom2  15740  fprodcnv  15949  fprodcom2  15950  invsym2  17725  oppcsect2  17741  cnvps  18537  tsrdir  18563  mvdco  19375  gsumcom2  19905  funcnvmpt  32591  fcnvgreu  32597  dfcnv2  32600  gsummpt2co  32988  gsumhashmul  33001  cnvco1  35746  cnvco2  35747  colinrel  36045  trer  36304  releleccnv  38246  eleccnvep  38269  brcnvrabga  38324  cnvresrn  38330  ineccnvmo  38339  elec1cnvxrn2  38383  cnvelrels  38486  dfdisjALTV  38705  dfeldisj5  38713  dfantisymrel4  38753  dfantisymrel5  38754  cnvnonrel  43577  cnvcnvintabd  43589  cnvintabd  43592  cnvssco  43595  clrellem  43611  clcnvlem  43612  cnviun  43639  trrelsuperrel2dg  43660  dffrege115  43967  dmtposss  48864  tposrescnv  48867  tposres3  48869  tposideq  48876