Theorem relcnv 6105

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

This proof depends on syntax axioms:   class class class wbr 5108  ^◡ccnv 5659  Rel wrel 5665

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-opab 5173  df-xp 5666  df-rel 5667  df-cnv 5668

This theorem is used by:  relbrcnvg  6106  eliniseg2  6107  cnvsym  6113  intasym  6114  asymref  6115  cnvopab  6136  cnvdif  6139  dfrel2  6186  cnvcnv  6189  cnvsn0  6210  cnvcnvsn  6219  resdm2  6231  coi2  6264  coires1  6265  cnvssrndm  6272  unidmrn  6280  cnviin  6287  predep  6331  funi  6568  funcnvsn  6586  funcnv2  6604  fcnvres  6755  f1cnvcnv  6785  funcnvmpt  6991  f1ompt  7106  fliftcnv  7309  cnvexg  7919  cnvf1o  8104  fsplit  8110  reldmtpos  8228  dmtpos  8232  rntpos  8233  dftpos3  8238  dftpos4  8239  tpostpos  8240  tposf12  8245  ercnv  8714  cnvct  9029  omxpenlem  9064  domss2  9122  cnvfi  9158  cnvfiALT  9294  trclublem  15039  relexpaddg  15097  fsumcnv  15831  fsumcom2  15832  fprodcnv  16044  fprodcom2  16045  invsym2  17826  oppcsect2  17842  cnvps  18640  tsrdir  18666  mvdco  19521  gsumcom2  20051  fcnvgreu  33028  dfcnv2  33031  gsummpt2co  33377  gsumhashmul  33396  cnvco1  36259  cnvco2  36260  colinrel  36557  trer  36855  releleccnv  38937  elec1cnvres  38952  eleccnvep  38964  brcnvrabga  39019  cnvresrn  39025  ineccnvmo  39034  elec1cnvxrn2  39097  dfsucmap3  39140  cnvelrels  39253  dfdisjALTV  39475  dfeldisj5  39490  dfantisymrel4  39541  dfantisymrel5  39542  cnvnonrel  44342  cnvcnvintabd  44354  cnvintabd  44357  cnvssco  44360  clrellem  44376  clcnvlem  44377  cnviun  44404  trrelsuperrel2dg  44425  dffrege115  44732  dmtposss  49682  tposrescnv  49685  tposres3  49687  tposideq  49694