Theorem relcnv 6103

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

Syntax hints:   class class class wbr 5148  ^◡ccnv 5675  Rel wrel 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-opab 5211  df-xp 5682  df-rel 5683  df-cnv 5684

This theorem is referenced by:  relbrcnvg  6104  eliniseg2  6105  cnvsym  6113  cnvsymOLD  6114  cnvsymOLDOLD  6115  intasym  6116  asymref  6117  cnvopab  6138  cnvdif  6143  dfrel2  6188  cnvcnv  6191  cnvsn0  6209  cnvcnvsn  6218  resdm2  6230  coi2  6262  coires1  6263  cnvssrndm  6270  unidmrn  6278  cnviin  6285  predep  6331  funi  6580  funcnvsn  6598  funcnv2  6616  fcnvres  6768  f1cnvcnv  6797  f1ompt  7110  fliftcnv  7307  cnvexg  7914  cnvf1o  8096  fsplit  8102  reldmtpos  8218  dmtpos  8222  rntpos  8223  dftpos3  8228  dftpos4  8229  tpostpos  8230  tposf12  8235  ercnv  8723  cnvct  9033  omxpenlem  9072  domss2  9135  cnvfi  9179  cnvfiALT  9333  trclublem  14941  relexpaddg  14999  fsumcnv  15718  fsumcom2  15719  fprodcnv  15926  fprodcom2  15927  invsym2  17709  oppcsect2  17725  cnvps  18530  tsrdir  18556  mvdco  19312  gsumcom2  19842  funcnvmpt  31887  fcnvgreu  31893  dfcnv2  31896  gsummpt2co  32195  gsumhashmul  32203  cnvco1  34724  cnvco2  34725  colinrel  35024  trer  35196  releleccnv  37120  eleccnvep  37144  brcnvrabga  37206  cnvresrn  37212  ineccnvmo  37221  elec1cnvxrn2  37262  cnvelrels  37360  dfdisjALTV  37578  dfeldisj5  37586  dfantisymrel4  37626  dfantisymrel5  37627  cnvnonrel  42329  cnvcnvintabd  42341  cnvintabd  42344  cnvssco  42347  clrellem  42363  clcnvlem  42364  cnviun  42391  trrelsuperrel2dg  42412  dffrege115  42719