Theorem relcnv 6078

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

Syntax hints:   class class class wbr 5110  ^◡ccnv 5640  Rel wrel 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649

This theorem is referenced by:  relbrcnvg  6079  eliniseg2  6080  cnvsym  6088  cnvsymOLD  6089  cnvsymOLDOLD  6090  intasym  6091  asymref  6092  cnvopab  6113  cnvopabOLD  6114  cnvdif  6119  dfrel2  6165  cnvcnv  6168  cnvsn0  6186  cnvcnvsn  6195  resdm2  6207  coi2  6239  coires1  6240  cnvssrndm  6247  unidmrn  6255  cnviin  6262  predep  6306  funi  6551  funcnvsn  6569  funcnv2  6587  fcnvres  6740  f1cnvcnv  6768  f1ompt  7086  fliftcnv  7289  cnvexg  7903  cnvf1o  8093  fsplit  8099  reldmtpos  8216  dmtpos  8220  rntpos  8221  dftpos3  8226  dftpos4  8227  tpostpos  8228  tposf12  8233  ercnv  8695  cnvct  9008  omxpenlem  9047  domss2  9106  cnvfi  9146  cnvfiALT  9297  trclublem  14968  relexpaddg  15026  fsumcnv  15746  fsumcom2  15747  fprodcnv  15956  fprodcom2  15957  invsym2  17732  oppcsect2  17748  cnvps  18544  tsrdir  18570  mvdco  19382  gsumcom2  19912  funcnvmpt  32598  fcnvgreu  32604  dfcnv2  32607  gsummpt2co  32995  gsumhashmul  33008  cnvco1  35753  cnvco2  35754  colinrel  36052  trer  36311  releleccnv  38253  eleccnvep  38276  brcnvrabga  38331  cnvresrn  38337  ineccnvmo  38346  elec1cnvxrn2  38390  cnvelrels  38493  dfdisjALTV  38712  dfeldisj5  38720  dfantisymrel4  38760  dfantisymrel5  38761  cnvnonrel  43584  cnvcnvintabd  43596  cnvintabd  43599  cnvssco  43602  clrellem  43618  clcnvlem  43619  cnviun  43646  trrelsuperrel2dg  43667  dffrege115  43974  dmtposss  48868  tposrescnv  48871  tposres3  48873  tposideq  48880