Theorem relcnv 5961

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

Syntax hints:   class class class wbr 5058  ^◡ccnv 5548  Rel wrel 5554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-opab 5121  df-xp 5555  df-rel 5556  df-cnv 5557

This theorem is referenced by:  relbrcnvg  5962  eliniseg2  5963  cnvsym  5968  intasym  5969  asymref  5970  cnvopab  5991  cnvdif  5996  dfrel2  6040  cnvcnv  6043  cnvsn0  6061  cnvcnvsn  6070  resdm2  6082  coi2  6110  coires1  6111  cnvssrndm  6116  unidmrn  6124  cnviin  6131  predep  6168  funi  6381  funcnvsn  6398  funcnv2  6416  fcnvres  6550  f1cnvcnv  6578  f1ompt  6869  fliftcnv  7058  cnvexg  7623  cnvf1o  7800  fsplit  7806  fsplitOLD  7807  reldmtpos  7894  dmtpos  7898  rntpos  7899  dftpos3  7904  dftpos4  7905  tpostpos  7906  tposf12  7911  ercnv  8304  cnvct  8580  omxpenlem  8612  domss2  8670  cnvfi  8800  trclublem  14349  relexpaddg  14406  fsumcnv  15122  fsumcom2  15123  fprodcnv  15331  fprodcom2  15332  invsym2  17027  oppcsect2  17043  cnvps  17816  tsrdir  17842  mvdco  18567  gsumcom2  19089  funcnvmpt  30406  fcnvgreu  30412  dfcnv2  30416  gsummpt2co  30681  cnvco1  32990  cnvco2  32991  colinrel  33513  trer  33659  releleccnv  35512  eleccnvep  35532  brcnvrabga  35593  cnvresrn  35599  ineccnvmo  35605  elec1cnvxrn2  35639  cnvelrels  35729  dfdisjALTV  35940  dfeldisj5  35948  cnvnonrel  39941  cnvcnvintabd  39953  cnvintabd  39956  cnvssco  39959  clrellem  39975  clcnvlem  39976  cnviun  39988  trrelsuperrel2dg  40009  dffrege115  40317