Theorem relcnv 6124

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

Syntax hints:   class class class wbr 5147  ^◡ccnv 5687  Rel wrel 5693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-opab 5210  df-xp 5694  df-rel 5695  df-cnv 5696

This theorem is referenced by:  relbrcnvg  6125  eliniseg2  6126  cnvsym  6134  cnvsymOLD  6135  cnvsymOLDOLD  6136  intasym  6137  asymref  6138  cnvopab  6159  cnvopabOLD  6160  cnvdif  6165  dfrel2  6210  cnvcnv  6213  cnvsn0  6231  cnvcnvsn  6240  resdm2  6252  coi2  6284  coires1  6285  cnvssrndm  6292  unidmrn  6300  cnviin  6307  predep  6352  funi  6599  funcnvsn  6617  funcnv2  6635  fcnvres  6785  f1cnvcnv  6813  f1ompt  7130  fliftcnv  7330  cnvexg  7946  cnvf1o  8134  fsplit  8140  reldmtpos  8257  dmtpos  8261  rntpos  8262  dftpos3  8267  dftpos4  8268  tpostpos  8269  tposf12  8274  ercnv  8764  cnvct  9072  omxpenlem  9111  domss2  9174  cnvfi  9214  cnvfiALT  9376  trclublem  15030  relexpaddg  15088  fsumcnv  15805  fsumcom2  15806  fprodcnv  16015  fprodcom2  16016  invsym2  17810  oppcsect2  17826  cnvps  18635  tsrdir  18661  mvdco  19477  gsumcom2  20007  funcnvmpt  32683  fcnvgreu  32689  dfcnv2  32692  gsummpt2co  33033  gsumhashmul  33046  cnvco1  35738  cnvco2  35739  colinrel  36038  trer  36298  releleccnv  38238  eleccnvep  38262  brcnvrabga  38323  cnvresrn  38329  ineccnvmo  38338  elec1cnvxrn2  38378  cnvelrels  38476  dfdisjALTV  38694  dfeldisj5  38702  dfantisymrel4  38742  dfantisymrel5  38743  cnvnonrel  43577  cnvcnvintabd  43589  cnvintabd  43592  cnvssco  43595  clrellem  43611  clcnvlem  43612  cnviun  43639  trrelsuperrel2dg  43660  dffrege115  43967