Theorem relcnv 6111

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

This proof depends on syntax axioms:   class class class wbr 5106  ^◡ccnv 5654  Rel wrel 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-opab 5171  df-xp 5661  df-rel 5662  df-cnv 5663

This theorem is used by:  relbrcnvg  6112  eliniseg2  6113  cnvsym  6119  intasym  6120  asymref  6121  cnvopab  6142  cnvdif  6145  cnvxp  6158  dfrel2  6192  cnvcnv  6195  cnvsn0  6223  cnvcnvsn  6232  resdm2  6244  coi2  6279  coires1  6280  cnvssrndm  6288  unidmrn  6297  cnviin  6304  predep  6348  funi  6589  funcnvsn  6609  funcnv2  6627  fcnvres  6778  f1cnvcnv  6808  funcnvmpt  7015  f1ompt  7132  fliftcnv  7339  cnvexg  7957  cnvf1o  8146  fsplit  8152  reldmtpos  8276  dmtpos  8280  rntpos  8281  dftpos3  8286  dftpos4  8287  tpostpos  8288  tposf12  8293  ercnv  8764  cnvct  9087  omxpenlem  9122  domss2  9180  cnvfi  9216  cnvfiALT  9353  trclublem  15174  relexpaddg  15232  fsumcnv  15965  fsumcom2  15966  fprodcnv  16176  fprodcom2  16177  invsym2  17964  oppcsect2  17980  cnvps  18778  tsrdir  18804  mvdco  19686  gsumcom2  20216  fcnvgreu  33335  dfcnv2  33337  gsummpt2co  33676  gsumhashmul  33695  cnvco1  36701  cnvco2  36702  colinrel  36999  trer  37281  releleccnv  39383  elec1cnvres  39398  eleccnvep  39410  brcnvrabga  39465  cnvresrn  39471  ineccnvmo  39480  elec1cnvxrn2  39543  dfsucmap3  39586  cnvelrels  39699  dfdisjALTV  39921  dfeldisj5  39936  dfantisymrel4  39987  dfantisymrel5  39988  cnvnonrel  44778  cnvcnvintabd  44790  cnvintabd  44793  cnvssco  44796  clrellem  44812  clcnvlem  44813  cnviun  44840  trrelsuperrel2dg  44861  dffrege115  45168  cocanss1  46114  dmtposss  50192  tposrescnv  50195  tposres3  50197  tposideq  50204