Theorem relcnv 6095

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

Syntax hints:   class class class wbr 5102  ^◡ccnv 5648  Rel wrel 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-opab 5165  df-xp 5655  df-rel 5656  df-cnv 5657

This theorem is referenced by:  relbrcnvg  6096  eliniseg2  6097  cnvsym  6103  intasym  6104  asymref  6105  cnvopab  6126  cnvdif  6129  dfrel2  6177  cnvcnv  6180  cnvsn0  6199  cnvcnvsn  6208  resdm2  6220  coi2  6253  coires1  6254  cnvssrndm  6260  unidmrn  6268  cnviin  6275  predep  6319  funi  6555  funcnvsn  6573  funcnv2  6591  fcnvres  6743  f1cnvcnv  6773  funcnvmpt  6979  f1ompt  7094  fliftcnv  7297  cnvexg  7907  cnvf1o  8092  fsplit  8098  reldmtpos  8216  dmtpos  8220  rntpos  8221  dftpos3  8226  dftpos4  8227  tpostpos  8228  tposf12  8233  ercnv  8702  cnvct  9017  omxpenlem  9052  domss2  9110  cnvfi  9146  cnvfiALT  9284  trclublem  15010  relexpaddg  15068  fsumcnv  15802  fsumcom2  15803  fprodcnv  16015  fprodcom2  16016  invsym2  17798  oppcsect2  17814  cnvps  18612  tsrdir  18638  mvdco  19487  gsumcom2  20017  fcnvgreu  32876  dfcnv2  32879  gsummpt2co  33230  gsumhashmul  33249  cnvco1  36114  cnvco2  36115  colinrel  36412  trer  36681  releleccnv  38764  elec1cnvres  38779  eleccnvep  38791  brcnvrabga  38846  cnvresrn  38852  ineccnvmo  38861  elec1cnvxrn2  38924  dfsucmap3  38967  cnvelrels  39080  dfdisjALTV  39302  dfeldisj5  39317  dfantisymrel4  39368  dfantisymrel5  39369  cnvnonrel  44169  cnvcnvintabd  44181  cnvintabd  44184  cnvssco  44187  clrellem  44203  clcnvlem  44204  cnviun  44231  trrelsuperrel2dg  44252  dffrege115  44559  dmtposss  49502  tposrescnv  49505  tposres3  49507  tposideq  49514