Theorem relcnv 6063

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

Syntax hints:   class class class wbr 5075  ^◡ccnv 5620  Rel wrel 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-opab 5138  df-xp 5627  df-rel 5628  df-cnv 5629

This theorem is referenced by:  relbrcnvg  6064  eliniseg2  6065  cnvsym  6071  intasym  6072  asymref  6073  cnvopab  6094  cnvopabOLD  6095  cnvdif  6098  dfrel2  6144  cnvcnv  6147  cnvsn0  6165  cnvcnvsn  6174  resdm2  6186  coi2  6219  coires1  6220  cnvssrndm  6226  unidmrn  6234  cnviin  6241  predep  6285  funi  6521  funcnvsn  6539  funcnv2  6557  fcnvres  6708  f1cnvcnv  6736  funcnvmpt  6941  f1ompt  7056  fliftcnv  7259  cnvexg  7868  cnvf1o  8054  fsplit  8060  reldmtpos  8178  dmtpos  8182  rntpos  8183  dftpos3  8188  dftpos4  8189  tpostpos  8190  tposf12  8195  ercnv  8659  cnvct  8975  omxpenlem  9010  domss2  9068  cnvfi  9104  cnvfiALT  9243  trclublem  14952  relexpaddg  15010  fsumcnv  15730  fsumcom2  15731  fprodcnv  15943  fprodcom2  15944  invsym2  17725  oppcsect2  17741  cnvps  18539  tsrdir  18565  mvdco  19415  gsumcom2  19945  fcnvgreu  32768  dfcnv2  32771  gsummpt2co  33133  gsumhashmul  33152  cnvco1  36002  cnvco2  36003  colinrel  36300  trer  36559  releleccnv  38642  elec1cnvres  38657  eleccnvep  38669  brcnvrabga  38724  cnvresrn  38730  ineccnvmo  38739  elec1cnvxrn2  38802  dfsucmap3  38845  cnvelrels  38958  dfdisjALTV  39180  dfeldisj5  39195  dfantisymrel4  39246  dfantisymrel5  39247  cnvnonrel  44047  cnvcnvintabd  44059  cnvintabd  44062  cnvssco  44065  clrellem  44081  clcnvlem  44082  cnviun  44109  trrelsuperrel2dg  44130  dffrege115  44437  dmtposss  49380  tposrescnv  49383  tposres3  49385  tposideq  49392