Theorem relcnv 6049

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

Syntax hints:   class class class wbr 5100  ^◡ccnv 5626  Rel wrel 5632

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 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-in 3912  df-ss 3922  df-opab 5163  df-xp 5633  df-rel 5634  df-cnv 5635

This theorem is referenced by:  relbrcnvg  6050  eliniseg2  6051  cnvsym  6059  cnvsymOLD  6060  cnvsymOLDOLD  6061  intasym  6062  asymref  6063  cnvopab  6084  cnvdif  6089  dfrel2  6134  cnvcnv  6137  cnvsn0  6155  cnvcnvsn  6164  resdm2  6176  coi2  6208  coires1  6209  cnvssrndm  6216  unidmrn  6224  cnviin  6231  predep  6277  funi  6525  funcnvsn  6543  funcnv2  6561  fcnvres  6711  f1cnvcnv  6740  f1ompt  7050  fliftcnv  7247  cnvexg  7848  cnvf1o  8028  fsplit  8034  reldmtpos  8129  dmtpos  8133  rntpos  8134  dftpos3  8139  dftpos4  8140  tpostpos  8141  tposf12  8146  ercnv  8599  cnvct  8908  omxpenlem  8947  domss2  9010  cnvfi  9054  cnvfiALT  9208  trclublem  14810  relexpaddg  14868  fsumcnv  15589  fsumcom2  15590  fprodcnv  15797  fprodcom2  15798  invsym2  17577  oppcsect2  17593  cnvps  18398  tsrdir  18424  mvdco  19154  gsumcom2  19675  funcnvmpt  31355  fcnvgreu  31361  dfcnv2  31364  gsummpt2co  31659  gsumhashmul  31667  cnvco1  34080  cnvco2  34081  colinrel  34498  trer  34644  releleccnv  36573  eleccnvep  36597  brcnvrabga  36659  cnvresrn  36665  ineccnvmo  36674  elec1cnvxrn2  36715  cnvelrels  36813  dfdisjALTV  37031  dfeldisj5  37039  dfantisymrel4  37079  dfantisymrel5  37080  cnvnonrel  41569  cnvcnvintabd  41581  cnvintabd  41584  cnvssco  41587  clrellem  41603  clcnvlem  41604  cnviun  41631  trrelsuperrel2dg  41652  dffrege115  41959