Theorem relcnv 6001

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

Syntax hints:   class class class wbr 5070  ^◡ccnv 5579  Rel wrel 5585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-opab 5133  df-xp 5586  df-rel 5587  df-cnv 5588

This theorem is referenced by:  relbrcnvg  6002  eliniseg2  6003  cnvsym  6008  intasym  6009  asymref  6010  cnvopab  6031  cnvdif  6036  dfrel2  6081  cnvcnv  6084  cnvsn0  6102  cnvcnvsn  6111  resdm2  6123  coi2  6156  coires1  6157  cnvssrndm  6163  unidmrn  6171  cnviin  6178  predep  6222  funi  6450  funcnvsn  6468  funcnv2  6486  fcnvres  6635  f1cnvcnv  6664  f1ompt  6967  fliftcnv  7162  cnvexg  7745  cnvf1o  7922  fsplit  7928  fsplitOLD  7929  reldmtpos  8021  dmtpos  8025  rntpos  8026  dftpos3  8031  dftpos4  8032  tpostpos  8033  tposf12  8038  ercnv  8477  cnvct  8778  omxpenlem  8813  domss2  8872  cnvfi  8924  cnvfiALT  9031  trclublem  14634  relexpaddg  14692  fsumcnv  15413  fsumcom2  15414  fprodcnv  15621  fprodcom2  15622  invsym2  17392  oppcsect2  17408  cnvps  18211  tsrdir  18237  mvdco  18968  gsumcom2  19491  funcnvmpt  30906  fcnvgreu  30912  dfcnv2  30915  gsummpt2co  31210  gsumhashmul  31218  cnvco1  33632  cnvco2  33633  colinrel  34286  trer  34432  releleccnv  36323  eleccnvep  36343  brcnvrabga  36404  cnvresrn  36410  ineccnvmo  36416  elec1cnvxrn2  36450  cnvelrels  36540  dfdisjALTV  36751  dfeldisj5  36759  cnvnonrel  41085  cnvcnvintabd  41097  cnvintabd  41100  cnvssco  41103  clrellem  41119  clcnvlem  41120  cnviun  41147  trrelsuperrel2dg  41168  dffrege115  41475