Theorem relcnv 6104

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

This proof depends on syntax axioms:   class class class wbr 5107  ^◡ccnv 5658  Rel wrel 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-opab 5172  df-xp 5665  df-rel 5666  df-cnv 5667

This theorem is used by:  relbrcnvg  6105  eliniseg2  6106  cnvsym  6112  intasym  6113  asymref  6114  cnvopab  6135  cnvdif  6138  cnvxp  6152  dfrel2  6186  cnvcnv  6189  cnvsn0  6210  cnvcnvsn  6219  resdm2  6231  coi2  6264  coires1  6265  cnvssrndm  6272  unidmrn  6281  cnviin  6288  predep  6332  funi  6569  funcnvsn  6587  funcnv2  6605  fcnvres  6756  f1cnvcnv  6786  funcnvmpt  6992  f1ompt  7107  fliftcnv  7315  cnvexg  7924  cnvf1o  8111  fsplit  8117  reldmtpos  8235  dmtpos  8239  rntpos  8240  dftpos3  8245  dftpos4  8246  tpostpos  8247  tposf12  8252  ercnv  8721  cnvct  9044  omxpenlem  9079  domss2  9137  cnvfi  9173  cnvfiALT  9309  trclublem  15070  relexpaddg  15128  fsumcnv  15861  fsumcom2  15862  fprodcnv  16074  fprodcom2  16075  invsym2  17856  oppcsect2  17872  cnvps  18670  tsrdir  18696  mvdco  19573  gsumcom2  20103  fcnvgreu  33132  dfcnv2  33135  gsummpt2co  33475  gsumhashmul  33494  cnvco1  36325  cnvco2  36326  colinrel  36624  trer  36922  releleccnv  38995  elec1cnvres  39010  eleccnvep  39022  brcnvrabga  39077  cnvresrn  39083  ineccnvmo  39092  elec1cnvxrn2  39155  dfsucmap3  39198  cnvelrels  39311  dfdisjALTV  39533  dfeldisj5  39548  dfantisymrel4  39599  dfantisymrel5  39600  cnvnonrel  44415  cnvcnvintabd  44427  cnvintabd  44430  cnvssco  44433  clrellem  44449  clcnvlem  44450  cnviun  44477  trrelsuperrel2dg  44498  dffrege115  44805  dmtposss  49789  tposrescnv  49792  tposres3  49794  tposideq  49801