Theorem relcnv 6122

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

Syntax hints:   class class class wbr 5143  ^◡ccnv 5684  Rel wrel 5690

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693

This theorem is referenced by:  relbrcnvg  6123  eliniseg2  6124  cnvsym  6132  cnvsymOLD  6133  cnvsymOLDOLD  6134  intasym  6135  asymref  6136  cnvopab  6157  cnvopabOLD  6158  cnvdif  6163  dfrel2  6209  cnvcnv  6212  cnvsn0  6230  cnvcnvsn  6239  resdm2  6251  coi2  6283  coires1  6284  cnvssrndm  6291  unidmrn  6299  cnviin  6306  predep  6351  funi  6598  funcnvsn  6616  funcnv2  6634  fcnvres  6785  f1cnvcnv  6813  f1ompt  7131  fliftcnv  7331  cnvexg  7946  cnvf1o  8136  fsplit  8142  reldmtpos  8259  dmtpos  8263  rntpos  8264  dftpos3  8269  dftpos4  8270  tpostpos  8271  tposf12  8276  ercnv  8766  cnvct  9074  omxpenlem  9113  domss2  9176  cnvfi  9216  cnvfiALT  9379  trclublem  15034  relexpaddg  15092  fsumcnv  15809  fsumcom2  15810  fprodcnv  16019  fprodcom2  16020  invsym2  17807  oppcsect2  17823  cnvps  18623  tsrdir  18649  mvdco  19463  gsumcom2  19993  funcnvmpt  32677  fcnvgreu  32683  dfcnv2  32686  gsummpt2co  33051  gsumhashmul  33064  cnvco1  35759  cnvco2  35760  colinrel  36058  trer  36317  releleccnv  38258  eleccnvep  38282  brcnvrabga  38343  cnvresrn  38349  ineccnvmo  38358  elec1cnvxrn2  38398  cnvelrels  38496  dfdisjALTV  38714  dfeldisj5  38722  dfantisymrel4  38762  dfantisymrel5  38763  cnvnonrel  43601  cnvcnvintabd  43613  cnvintabd  43616  cnvssco  43619  clrellem  43635  clcnvlem  43636  cnviun  43663  trrelsuperrel2dg  43684  dffrege115  43991  dmtposss  48776  tposrescnv  48779  tposres3  48781  tposideq  48788