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

Syntax hints:   class class class wbr 5149  ^◡ccnv 5676  Rel wrel 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-opab 5212  df-xp 5683  df-rel 5684  df-cnv 5685

This theorem is referenced by:  relbrcnvg  6105  eliniseg2  6106  cnvsym  6114  cnvsymOLD  6115  cnvsymOLDOLD  6116  intasym  6117  asymref  6118  cnvopab  6139  cnvdif  6144  dfrel2  6189  cnvcnv  6192  cnvsn0  6210  cnvcnvsn  6219  resdm2  6231  coi2  6263  coires1  6264  cnvssrndm  6271  unidmrn  6279  cnviin  6286  predep  6332  funi  6581  funcnvsn  6599  funcnv2  6617  fcnvres  6769  f1cnvcnv  6798  f1ompt  7111  fliftcnv  7308  cnvexg  7915  cnvf1o  8097  fsplit  8103  reldmtpos  8219  dmtpos  8223  rntpos  8224  dftpos3  8229  dftpos4  8230  tpostpos  8231  tposf12  8236  ercnv  8724  cnvct  9034  omxpenlem  9073  domss2  9136  cnvfi  9180  cnvfiALT  9334  trclublem  14942  relexpaddg  15000  fsumcnv  15719  fsumcom2  15720  fprodcnv  15927  fprodcom2  15928  invsym2  17710  oppcsect2  17726  cnvps  18531  tsrdir  18557  mvdco  19313  gsumcom2  19843  funcnvmpt  31923  fcnvgreu  31929  dfcnv2  31932  gsummpt2co  32231  gsumhashmul  32239  cnvco1  34760  cnvco2  34761  colinrel  35060  trer  35249  releleccnv  37173  eleccnvep  37197  brcnvrabga  37259  cnvresrn  37265  ineccnvmo  37274  elec1cnvxrn2  37315  cnvelrels  37413  dfdisjALTV  37631  dfeldisj5  37639  dfantisymrel4  37679  dfantisymrel5  37680  cnvnonrel  42387  cnvcnvintabd  42399  cnvintabd  42402  cnvssco  42405  clrellem  42421  clcnvlem  42422  cnviun  42449  trrelsuperrel2dg  42470  dffrege115  42777