Theorem relcnv 5659

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

Syntax hints:   class class class wbr 4802  ^◡ccnv 5263  Rel wrel 5269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-rab 3057  df-v 3340  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-sn 4320  df-pr 4322  df-op 4326  df-opab 4863  df-xp 5270  df-rel 5271  df-cnv 5272

This theorem is referenced by:  relbrcnvg  5660  eliniseg2  5661  cnvsym  5666  intasym  5667  asymref  5668  cnvopab  5689  cnv0OLD  5692  cnvdif  5695  dfrel2  5739  cnvcnv  5742  cnvcnvOLD  5743  cnvsn0  5759  cnvcnvsn  5769  resdm2  5783  coi2  5811  coires1  5812  cnvssrndm  5816  unidmrn  5824  cnviin  5831  predep  5865  funi  6079  funcnvsn  6095  funcnv2  6116  fcnvres  6241  f1cnvcnv  6268  f1ompt  6543  fliftcnv  6722  cnvexg  7275  cnvf1o  7442  fsplit  7448  reldmtpos  7527  dmtpos  7531  rntpos  7532  dftpos3  7537  dftpos4  7538  tpostpos  7539  tposf12  7544  ercnv  7930  cnvct  8196  omxpenlem  8224  domss2  8282  cnvfi  8411  trclublem  13933  relexpaddg  13990  fsumcnv  14701  fsumcom2  14702  fsumcom2OLD  14703  fprodcnv  14910  fprodcom2  14911  fprodcom2OLD  14912  invsym2  16622  oppcsect2  16638  cnvps  17411  tsrdir  17437  mvdco  18063  gsumcom2  18572  funcnvmptOLD  29774  funcnvmpt  29775  fcnvgreu  29779  dfcnv2  29783  gsummpt2co  30087  cnvco1  31954  cnvco2  31955  colinrel  32468  trer  32614  releleccnv  34343  eleccnvep  34368  cnvresrn  34437  ineccnvmo  34443  elec1cnvxrn2  34476  cnvelrels  34566  cnvnonrel  38394  cnvcnvintabd  38406  cnvintabd  38409  cnvssco  38412  clrellem  38429  clcnvlem  38430  cnviun  38442  trrelsuperrel2dg  38463  dffrege115  38772