Theorem relcnv 6055

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

Syntax hints:   class class class wbr 5092  ^◡ccnv 5618  Rel wrel 5624

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-opab 5155  df-xp 5625  df-rel 5626  df-cnv 5627

This theorem is referenced by:  relbrcnvg  6056  eliniseg2  6057  cnvsym  6063  intasym  6064  asymref  6065  cnvopab  6086  cnvopabOLD  6087  cnvdif  6092  dfrel2  6138  cnvcnv  6141  cnvsn0  6159  cnvcnvsn  6168  resdm2  6180  coi2  6212  coires1  6213  cnvssrndm  6219  unidmrn  6227  cnviin  6234  predep  6278  funi  6514  funcnvsn  6532  funcnv2  6550  fcnvres  6701  f1cnvcnv  6729  f1ompt  7045  fliftcnv  7248  cnvexg  7857  cnvf1o  8044  fsplit  8050  reldmtpos  8167  dmtpos  8171  rntpos  8172  dftpos3  8177  dftpos4  8178  tpostpos  8179  tposf12  8184  ercnv  8646  cnvct  8959  omxpenlem  8995  domss2  9053  cnvfi  9090  cnvfiALT  9229  trclublem  14902  relexpaddg  14960  fsumcnv  15680  fsumcom2  15681  fprodcnv  15890  fprodcom2  15891  invsym2  17670  oppcsect2  17686  cnvps  18484  tsrdir  18510  mvdco  19324  gsumcom2  19854  funcnvmpt  32618  fcnvgreu  32624  dfcnv2  32627  gsummpt2co  33010  gsumhashmul  33023  cnvco1  35752  cnvco2  35753  colinrel  36051  trer  36310  releleccnv  38252  eleccnvep  38275  brcnvrabga  38330  cnvresrn  38336  ineccnvmo  38345  elec1cnvxrn2  38389  cnvelrels  38492  dfdisjALTV  38711  dfeldisj5  38719  dfantisymrel4  38759  dfantisymrel5  38760  cnvnonrel  43581  cnvcnvintabd  43593  cnvintabd  43596  cnvssco  43599  clrellem  43615  clcnvlem  43616  cnviun  43643  trrelsuperrel2dg  43664  dffrege115  43971  dmtposss  48880  tposrescnv  48883  tposres3  48885  tposideq  48892