Theorem relcnv 6134

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

Syntax hints:   class class class wbr 5166  ^◡ccnv 5699  Rel wrel 5705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-opab 5229  df-xp 5706  df-rel 5707  df-cnv 5708

This theorem is referenced by:  relbrcnvg  6135  eliniseg2  6136  cnvsym  6144  cnvsymOLD  6145  cnvsymOLDOLD  6146  intasym  6147  asymref  6148  cnvopab  6169  cnvopabOLD  6170  cnvdif  6175  dfrel2  6220  cnvcnv  6223  cnvsn0  6241  cnvcnvsn  6250  resdm2  6262  coi2  6294  coires1  6295  cnvssrndm  6302  unidmrn  6310  cnviin  6317  predep  6362  funi  6610  funcnvsn  6628  funcnv2  6646  fcnvres  6798  f1cnvcnv  6826  f1ompt  7145  fliftcnv  7347  cnvexg  7964  cnvf1o  8152  fsplit  8158  reldmtpos  8275  dmtpos  8279  rntpos  8280  dftpos3  8285  dftpos4  8286  tpostpos  8287  tposf12  8292  ercnv  8784  cnvct  9099  omxpenlem  9139  domss2  9202  cnvfi  9243  cnvfiALT  9407  trclublem  15044  relexpaddg  15102  fsumcnv  15821  fsumcom2  15822  fprodcnv  16031  fprodcom2  16032  invsym2  17824  oppcsect2  17840  cnvps  18648  tsrdir  18674  mvdco  19487  gsumcom2  20017  funcnvmpt  32685  fcnvgreu  32691  dfcnv2  32694  gsummpt2co  33031  gsumhashmul  33040  cnvco1  35721  cnvco2  35722  colinrel  36021  trer  36282  releleccnv  38213  eleccnvep  38237  brcnvrabga  38298  cnvresrn  38304  ineccnvmo  38313  elec1cnvxrn2  38353  cnvelrels  38451  dfdisjALTV  38669  dfeldisj5  38677  dfantisymrel4  38717  dfantisymrel5  38718  cnvnonrel  43550  cnvcnvintabd  43562  cnvintabd  43565  cnvssco  43568  clrellem  43584  clcnvlem  43585  cnviun  43612  trrelsuperrel2dg  43633  dffrege115  43940