Theorem relcnv 5503

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

Syntax hints:   class class class wbr 4653  ^◡ccnv 5113  Rel wrel 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122

This theorem is referenced by:  relbrcnvg  5504  eliniseg2  5505  cnvsym  5510  intasym  5511  asymref  5512  cnvopab  5533  cnv0OLD  5536  cnvdif  5539  dfrel2  5583  cnvcnv  5586  cnvcnvOLD  5587  cnvsn0  5603  cnvcnvsn  5612  resdm2  5624  coi2  5652  coires1  5653  cnvssrndm  5657  unidmrn  5665  cnviin  5672  predep  5706  funi  5920  funcnvsn  5936  funcnv2  5957  fcnvres  6082  f1cnvcnv  6109  f1ompt  6382  fliftcnv  6561  cnvexg  7112  cnvf1o  7276  fsplit  7282  reldmtpos  7360  dmtpos  7364  rntpos  7365  dftpos3  7370  dftpos4  7371  tpostpos  7372  tposf12  7377  ercnv  7763  cnvct  8033  omxpenlem  8061  domss2  8119  cnvfi  8248  trclublem  13734  relexpaddg  13793  fsumcnv  14504  fsumcom2  14505  fsumcom2OLD  14506  fprodcnv  14713  fprodcom2  14714  fprodcom2OLD  14715  invsym2  16423  oppcsect2  16439  cnvps  17212  tsrdir  17238  mvdco  17865  gsumcom2  18374  funcnvmptOLD  29467  funcnvmpt  29468  fcnvgreu  29472  dfcnv2  29476  gsummpt2co  29780  cnvco1  31649  cnvco2  31650  colinrel  32164  trer  32310  releleccnv  34021  eleccnvep  34046  cnvresrn  34116  ineccnvmo  34122  cnvnonrel  37894  cnvcnvintabd  37906  cnvintabd  37909  cnvssco  37912  clrellem  37929  clcnvlem  37930  cnviun  37942  trrelsuperrel2dg  37963  dffrege115  38272