Theorem relcnv 6058

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

Syntax hints:   class class class wbr 5074  ^◡ccnv 5619  Rel wrel 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3429  df-ss 3902  df-opab 5137  df-xp 5626  df-rel 5627  df-cnv 5628

This theorem is referenced by:  relbrcnvg  6059  eliniseg2  6060  cnvsym  6066  intasym  6067  asymref  6068  cnvopab  6089  cnvopabOLD  6090  cnvdif  6096  dfrel2  6142  cnvcnv  6145  cnvsn0  6163  cnvcnvsn  6172  resdm2  6184  coi2  6217  coires1  6218  cnvssrndm  6224  unidmrn  6232  cnviin  6239  predep  6283  funi  6519  funcnvsn  6537  funcnv2  6555  fcnvres  6706  f1cnvcnv  6734  funcnvmpt  6938  f1ompt  7052  fliftcnv  7255  cnvexg  7864  cnvf1o  8050  fsplit  8056  reldmtpos  8173  dmtpos  8177  rntpos  8178  dftpos3  8183  dftpos4  8184  tpostpos  8185  tposf12  8190  ercnv  8654  cnvct  8970  omxpenlem  9005  domss2  9063  cnvfi  9099  cnvfiALT  9238  trclublem  14946  relexpaddg  15004  fsumcnv  15724  fsumcom2  15725  fprodcnv  15937  fprodcom2  15938  invsym2  17719  oppcsect2  17735  cnvps  18533  tsrdir  18559  mvdco  19409  gsumcom2  19939  fcnvgreu  32733  dfcnv2  32736  gsummpt2co  33097  gsumhashmul  33116  cnvco1  35929  cnvco2  35930  colinrel  36227  trer  36486  releleccnv  38569  elec1cnvres  38584  eleccnvep  38596  brcnvrabga  38651  cnvresrn  38657  ineccnvmo  38666  elec1cnvxrn2  38729  dfsucmap3  38772  cnvelrels  38885  dfdisjALTV  39107  dfeldisj5  39122  dfantisymrel4  39173  dfantisymrel5  39174  cnvnonrel  44003  cnvcnvintabd  44015  cnvintabd  44018  cnvssco  44021  clrellem  44037  clcnvlem  44038  cnviun  44065  trrelsuperrel2dg  44086  dffrege115  44393  dmtposss  49339  tposrescnv  49342  tposres3  49344  tposideq  49351