Theorem relcnv 5952

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

Syntax hints:   class class class wbr 5039  ^◡ccnv 5535  Rel wrel 5541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-opab 5102  df-xp 5542  df-rel 5543  df-cnv 5544

This theorem is referenced by:  relbrcnvg  5953  eliniseg2  5954  cnvsym  5959  intasym  5960  asymref  5961  cnvopab  5982  cnvdif  5987  dfrel2  6032  cnvcnv  6035  cnvsn0  6053  cnvcnvsn  6062  resdm2  6074  coi2  6107  coires1  6108  cnvssrndm  6114  unidmrn  6122  cnviin  6129  predep  6166  funi  6390  funcnvsn  6408  funcnv2  6426  fcnvres  6574  f1cnvcnv  6603  f1ompt  6906  fliftcnv  7098  cnvexg  7680  cnvf1o  7857  fsplit  7863  fsplitOLD  7864  reldmtpos  7954  dmtpos  7958  rntpos  7959  dftpos3  7964  dftpos4  7965  tpostpos  7966  tposf12  7971  ercnv  8390  cnvct  8689  omxpenlem  8724  domss2  8783  cnvfi  8834  cnvfiALT  8936  trclublem  14523  relexpaddg  14581  fsumcnv  15300  fsumcom2  15301  fprodcnv  15508  fprodcom2  15509  invsym2  17222  oppcsect2  17238  cnvps  18038  tsrdir  18064  mvdco  18791  gsumcom2  19314  funcnvmpt  30678  fcnvgreu  30684  dfcnv2  30687  gsummpt2co  30981  gsumhashmul  30989  cnvco1  33396  cnvco2  33397  colinrel  34045  trer  34191  releleccnv  36082  eleccnvep  36102  brcnvrabga  36163  cnvresrn  36169  ineccnvmo  36175  elec1cnvxrn2  36209  cnvelrels  36299  dfdisjALTV  36510  dfeldisj5  36518  cnvnonrel  40813  cnvcnvintabd  40825  cnvintabd  40828  cnvssco  40831  clrellem  40847  clcnvlem  40848  cnviun  40876  trrelsuperrel2dg  40897  dffrege115  41204