Theorem relcnv 5061

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

Syntax hints:   class class class wbr 4045  ^◡ccnv 4675  Rel wrel 4681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219  ax-pr 4254

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-opab 4107  df-xp 4682  df-rel 4683  df-cnv 4684

This theorem is referenced by:  relbrcnvg  5062  eliniseg2  5063  cnvsym  5067  intasym  5068  asymref  5069  cnvopab  5085  cnv0  5087  cnvdif  5090  dfrel2  5134  cnvcnv  5136  cnvsn0  5152  cnvcnvsn  5160  resdm2  5174  coi2  5200  coires1  5201  cnvssrndm  5205  unidmrn  5216  cnvexg  5221  cnviinm  5225  funi  5304  funcnvsn  5320  funcnv2  5335  funcnveq  5338  fcnvres  5461  f1cnvcnv  5494  f1ompt  5733  fliftcnv  5866  cnvf1o  6313  reldmtpos  6341  dmtpos  6344  rntpos  6345  dftpos3  6350  dftpos4  6351  tpostpos  6352  tposf12  6357  ercnv  6643  cnvct  6903  relcnvfi  7045  fsumcnv  11781  fisumcom2  11782  fprodcnv  11969  fprodcom2fi  11970