Theorem relcnv 6064

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

Syntax hints:   class class class wbr 5099  ^◡ccnv 5624  Rel wrel 5630

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-ss 3919  df-opab 5162  df-xp 5631  df-rel 5632  df-cnv 5633

This theorem is referenced by:  relbrcnvg  6065  eliniseg2  6066  cnvsym  6072  intasym  6073  asymref  6074  cnvopab  6095  cnvopabOLD  6096  cnvdif  6102  dfrel2  6148  cnvcnv  6151  cnvsn0  6169  cnvcnvsn  6178  resdm2  6190  coi2  6223  coires1  6224  cnvssrndm  6230  unidmrn  6238  cnviin  6245  predep  6289  funi  6525  funcnvsn  6543  funcnv2  6561  fcnvres  6712  f1cnvcnv  6740  funcnvmpt  6944  f1ompt  7058  fliftcnv  7260  cnvexg  7869  cnvf1o  8056  fsplit  8062  reldmtpos  8179  dmtpos  8183  rntpos  8184  dftpos3  8189  dftpos4  8190  tpostpos  8191  tposf12  8196  ercnv  8660  cnvct  8976  omxpenlem  9011  domss2  9069  cnvfi  9105  cnvfiALT  9244  trclublem  14923  relexpaddg  14981  fsumcnv  15701  fsumcom2  15702  fprodcnv  15911  fprodcom2  15912  invsym2  17692  oppcsect2  17708  cnvps  18506  tsrdir  18532  mvdco  19379  gsumcom2  19909  fcnvgreu  32754  dfcnv2  32757  gsummpt2co  33134  gsumhashmul  33153  cnvco1  35966  cnvco2  35967  colinrel  36264  trer  36523  releleccnv  38474  elec1cnvres  38489  eleccnvep  38501  brcnvrabga  38556  cnvresrn  38562  ineccnvmo  38571  elec1cnvxrn2  38634  dfsucmap3  38677  cnvelrels  38790  dfdisjALTV  39012  dfeldisj5  39027  dfantisymrel4  39078  dfantisymrel5  39079  cnvnonrel  43907  cnvcnvintabd  43919  cnvintabd  43922  cnvssco  43925  clrellem  43941  clcnvlem  43942  cnviun  43969  trrelsuperrel2dg  43990  dffrege115  44297  dmtposss  49198  tposrescnv  49201  tposres3  49203  tposideq  49210