Theorem relcnv 5409

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

Syntax hints:   class class class wbr 4577  ^◡ccnv 5027  Rel wrel 5033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-opab 4638  df-xp 5034  df-rel 5035  df-cnv 5036

This theorem is referenced by:  relbrcnvg  5410  eliniseg2  5411  cnvsym  5416  intasym  5417  asymref  5418  cnvopab  5439  cnv0  5441  cnvdif  5444  dfrel2  5488  cnvcnv  5491  cnvsn0  5507  cnvcnvsn  5516  resdm2  5528  coi2  5555  coires1  5556  cnvssrndm  5560  unidmrn  5568  cnviin  5575  predep  5609  funi  5820  funcnvsn  5836  funcnv2  5857  fcnvres  5980  f1cnvcnv  6007  f1ompt  6275  fliftcnv  6439  cnvexg  6983  cnvf1o  7141  fsplit  7147  reldmtpos  7225  dmtpos  7229  rntpos  7230  dftpos3  7235  dftpos4  7236  tpostpos  7237  tposf12  7242  ercnv  7628  omxpenlem  7924  domss2  7982  cnvfi  8109  trclublem  13531  relexpaddg  13590  fsumcnv  14295  fsumcom2  14296  fsumcom2OLD  14297  fprodcnv  14501  fprodcom2  14502  fprodcom2OLD  14503  invsym2  16195  oppcsect2  16211  cnvps  16984  tsrdir  17010  mvdco  17637  gsumcom2  18146  funcnvmptOLD  28684  funcnvmpt  28685  fcnvgreu  28689  dfcnv2  28693  cnvct  28712  gsummpt2co  28945  cnvco1  30737  cnvco2  30738  colinrel  31168  trer  31314  cnvnonrel  36737  cnvcnvintabd  36749  cnvintabd  36752  cnvssco  36755  clrellem  36772  clcnvlem  36773  cnviun  36785  trrelsuperrel2dg  36806  dffrege115  37116