Theorem relcnv 6117

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

Syntax hints:   class class class wbr 5154  ^◡ccnv 5683  Rel wrel 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-v 3474  df-ss 3975  df-opab 5217  df-xp 5690  df-rel 5691  df-cnv 5692

This theorem is referenced by:  relbrcnvg  6118  eliniseg2  6119  cnvsym  6127  cnvsymOLD  6128  cnvsymOLDOLD  6129  intasym  6130  asymref  6131  cnvopab  6152  cnvopabOLD  6153  cnvdif  6158  dfrel2  6203  cnvcnv  6206  cnvsn0  6224  cnvcnvsn  6233  resdm2  6245  coi2  6277  coires1  6278  cnvssrndm  6285  unidmrn  6293  cnviin  6300  predep  6345  funi  6593  funcnvsn  6611  funcnv2  6629  fcnvres  6781  f1cnvcnv  6809  f1ompt  7127  fliftcnv  7326  cnvexg  7942  cnvf1o  8130  fsplit  8136  reldmtpos  8253  dmtpos  8257  rntpos  8258  dftpos3  8263  dftpos4  8264  tpostpos  8265  tposf12  8270  ercnv  8759  cnvct  9074  omxpenlem  9114  domss2  9177  cnvfi  9218  cnvfiALT  9382  trclublem  15013  relexpaddg  15071  fsumcnv  15790  fsumcom2  15791  fprodcnv  15998  fprodcom2  15999  invsym2  17792  oppcsect2  17808  cnvps  18616  tsrdir  18642  mvdco  19455  gsumcom2  19985  funcnvmpt  32585  fcnvgreu  32591  dfcnv2  32594  gsummpt2co  32931  gsumhashmul  32940  cnvco1  35621  cnvco2  35622  colinrel  35921  trer  36069  releleccnv  37995  eleccnvep  38019  brcnvrabga  38080  cnvresrn  38086  ineccnvmo  38095  elec1cnvxrn2  38135  cnvelrels  38233  dfdisjALTV  38451  dfeldisj5  38459  dfantisymrel4  38499  dfantisymrel5  38500  cnvnonrel  43322  cnvcnvintabd  43334  cnvintabd  43337  cnvssco  43340  clrellem  43356  clcnvlem  43357  cnviun  43384  trrelsuperrel2dg  43405  dffrege115  43712