Theorem relcnv 6099

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

This proof depends on syntax axioms:   class class class wbr 5102  ^◡ccnv 5649  Rel wrel 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658

This theorem is used by:  relbrcnvg  6100  eliniseg2  6101  cnvsym  6107  intasym  6108  asymref  6109  cnvopab  6130  cnvdif  6133  cnvxp  6146  dfrel2  6180  cnvcnv  6183  cnvsn0  6211  cnvcnvsn  6220  resdm2  6232  coi2  6265  coires1  6266  cnvssrndm  6273  unidmrn  6282  cnviin  6289  predep  6333  funi  6572  funcnvsn  6590  funcnv2  6608  fcnvres  6759  f1cnvcnv  6789  funcnvmpt  6995  f1ompt  7111  fliftcnv  7319  cnvexg  7936  cnvf1o  8122  fsplit  8128  reldmtpos  8251  dmtpos  8255  rntpos  8256  dftpos3  8261  dftpos4  8262  tpostpos  8263  tposf12  8268  ercnv  8739  cnvct  9062  omxpenlem  9097  domss2  9155  cnvfi  9191  cnvfiALT  9328  trclublem  15148  relexpaddg  15206  fsumcnv  15939  fsumcom2  15940  fprodcnv  16150  fprodcom2  16151  invsym2  17938  oppcsect2  17954  cnvps  18752  tsrdir  18778  mvdco  19659  gsumcom2  20189  fcnvgreu  33266  dfcnv2  33269  gsummpt2co  33609  gsumhashmul  33628  cnvco1  36524  cnvco2  36525  colinrel  36822  trer  37104  releleccnv  39193  elec1cnvres  39208  eleccnvep  39220  brcnvrabga  39275  cnvresrn  39281  ineccnvmo  39290  elec1cnvxrn2  39353  dfsucmap3  39396  cnvelrels  39509  dfdisjALTV  39731  dfeldisj5  39746  dfantisymrel4  39797  dfantisymrel5  39798  cnvnonrel  44588  cnvcnvintabd  44600  cnvintabd  44603  cnvssco  44606  clrellem  44622  clcnvlem  44623  cnviun  44650  trrelsuperrel2dg  44671  dffrege115  44978  cocanss1  45924  dmtposss  49984  tposrescnv  49987  tposres3  49989  tposideq  49996