Theorem relcnv 6012

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

Syntax hints:   class class class wbr 5074  ^◡ccnv 5588  Rel wrel 5594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-opab 5137  df-xp 5595  df-rel 5596  df-cnv 5597

This theorem is referenced by:  relbrcnvg  6013  eliniseg2  6014  cnvsym  6019  intasym  6020  asymref  6021  cnvopab  6042  cnvdif  6047  dfrel2  6092  cnvcnv  6095  cnvsn0  6113  cnvcnvsn  6122  resdm2  6134  coi2  6167  coires1  6168  cnvssrndm  6174  unidmrn  6182  cnviin  6189  predep  6233  funi  6466  funcnvsn  6484  funcnv2  6502  fcnvres  6651  f1cnvcnv  6680  f1ompt  6985  fliftcnv  7182  cnvexg  7771  cnvf1o  7951  fsplit  7957  fsplitOLD  7958  reldmtpos  8050  dmtpos  8054  rntpos  8055  dftpos3  8060  dftpos4  8061  tpostpos  8062  tposf12  8067  ercnv  8519  cnvct  8824  omxpenlem  8860  domss2  8923  cnvfi  8963  cnvfiALT  9101  trclublem  14706  relexpaddg  14764  fsumcnv  15485  fsumcom2  15486  fprodcnv  15693  fprodcom2  15694  invsym2  17475  oppcsect2  17491  cnvps  18296  tsrdir  18322  mvdco  19053  gsumcom2  19576  funcnvmpt  31004  fcnvgreu  31010  dfcnv2  31013  gsummpt2co  31308  gsumhashmul  31316  cnvco1  33726  cnvco2  33727  colinrel  34359  trer  34505  releleccnv  36396  eleccnvep  36416  brcnvrabga  36477  cnvresrn  36483  ineccnvmo  36489  elec1cnvxrn2  36523  cnvelrels  36613  dfdisjALTV  36824  dfeldisj5  36832  cnvnonrel  41196  cnvcnvintabd  41208  cnvintabd  41211  cnvssco  41214  clrellem  41230  clcnvlem  41231  cnviun  41258  trrelsuperrel2dg  41279  dffrege115  41586