Theorem relcnv 6094

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

This proof depends on syntax axioms:   class class class wbr 5102  ^◡ccnv 5646  Rel wrel 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3915  df-opab 5167  df-xp 5653  df-rel 5654  df-cnv 5655

This theorem is used by:  relbrcnvg  6095  eliniseg2  6096  cnvsym  6102  intasym  6103  asymref  6104  cnvopab  6125  cnvdif  6128  cnvxp  6142  dfrel2  6176  cnvcnv  6179  cnvsn0  6200  cnvcnvsn  6209  resdm2  6221  coi2  6254  coires1  6255  cnvssrndm  6262  unidmrn  6271  cnviin  6278  predep  6322  funi  6560  funcnvsn  6578  funcnv2  6596  fcnvres  6747  f1cnvcnv  6777  funcnvmpt  6983  f1ompt  7099  fliftcnv  7307  cnvexg  7919  cnvf1o  8105  fsplit  8111  reldmtpos  8229  dmtpos  8233  rntpos  8234  dftpos3  8239  dftpos4  8240  tpostpos  8241  tposf12  8246  ercnv  8717  cnvct  9040  omxpenlem  9075  domss2  9133  cnvfi  9169  cnvfiALT  9306  trclublem  15115  relexpaddg  15173  fsumcnv  15906  fsumcom2  15907  fprodcnv  16117  fprodcom2  16118  invsym2  17899  oppcsect2  17915  cnvps  18713  tsrdir  18739  mvdco  19620  gsumcom2  20150  fcnvgreu  33199  dfcnv2  33202  gsummpt2co  33542  gsumhashmul  33561  cnvco1  36445  cnvco2  36446  colinrel  36744  trer  37026  releleccnv  39112  elec1cnvres  39127  eleccnvep  39139  brcnvrabga  39194  cnvresrn  39200  ineccnvmo  39209  elec1cnvxrn2  39272  dfsucmap3  39315  cnvelrels  39428  dfdisjALTV  39650  dfeldisj5  39665  dfantisymrel4  39716  dfantisymrel5  39717  cnvnonrel  44532  cnvcnvintabd  44544  cnvintabd  44547  cnvssco  44550  clrellem  44566  clcnvlem  44567  cnviun  44594  trrelsuperrel2dg  44615  dffrege115  44922  dmtposss  49906  tposrescnv  49909  tposres3  49911  tposideq  49918