Theorem relcnv 5850

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

Syntax hints:   class class class wbr 4968  ^◡ccnv 5449  Rel wrel 5455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-opab 5031  df-xp 5456  df-rel 5457  df-cnv 5458

This theorem is referenced by:  relbrcnvg  5851  eliniseg2  5852  cnvsym  5857  intasym  5858  asymref  5859  cnvopab  5880  cnvdif  5885  dfrel2  5929  cnvcnv  5932  cnvsn0  5949  cnvcnvsn  5958  resdm2  5970  coi2  5998  coires1  5999  cnvssrndm  6004  unidmrn  6012  cnviin  6019  predep  6056  funi  6264  funcnvsn  6281  funcnv2  6299  fcnvres  6431  f1cnvcnv  6459  f1ompt  6745  fliftcnv  6934  cnvexg  7492  cnvf1o  7669  fsplit  7675  reldmtpos  7758  dmtpos  7762  rntpos  7763  dftpos3  7768  dftpos4  7769  tpostpos  7770  tposf12  7775  ercnv  8167  cnvct  8441  omxpenlem  8472  domss2  8530  cnvfi  8659  trclublem  14193  relexpaddg  14250  fsumcnv  14965  fsumcom2  14966  fprodcnv  15174  fprodcom2  15175  invsym2  16866  oppcsect2  16882  cnvps  17655  tsrdir  17681  mvdco  18308  gsumcom2  18819  funcnvmpt  30098  fcnvgreu  30104  dfcnv2  30108  gsummpt2co  30491  cnvco1  32605  cnvco2  32606  colinrel  33129  trer  33275  releleccnv  35071  eleccnvep  35091  brcnvrabga  35152  cnvresrn  35158  ineccnvmo  35164  elec1cnvxrn2  35197  cnvelrels  35287  dfdisjALTV  35498  dfeldisj5  35506  cnvnonrel  39454  cnvcnvintabd  39466  cnvintabd  39469  cnvssco  39472  clrellem  39488  clcnvlem  39489  cnviun  39501  trrelsuperrel2dg  39522  dffrege115  39830