Theorem relcnv 5007

Description: A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed by NM, 29-Oct-1996.)

Assertion

Ref	Expression
relcnv	|- Rel `' A

Proof of Theorem relcnv

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-cnv 4635	. 2 |- `' A = { <. x , y >. | y A x }
2	1	relopabi 4753	1 |- Rel `' A

Syntax hints:   class class class wbr 4004   `'ccnv 4626   Rel wrel 4632

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-opab 4066  df-xp 4633  df-rel 4634  df-cnv 4635

This theorem is referenced by:  relbrcnvg  5008  eliniseg2  5009  cnvsym  5013  intasym  5014  asymref  5015  cnvopab  5031  cnv0  5033  cnvdif  5036  dfrel2  5080  cnvcnv  5082  cnvsn0  5098  cnvcnvsn  5106  resdm2  5120  coi2  5146  coires1  5147  cnvssrndm  5151  unidmrn  5162  cnvexg  5167  cnviinm  5171  funi  5249  funcnvsn  5262  funcnv2  5277  funcnveq  5280  fcnvres  5400  f1cnvcnv  5433  f1ompt  5668  fliftcnv  5796  cnvf1o  6226  reldmtpos  6254  dmtpos  6257  rntpos  6258  dftpos3  6263  dftpos4  6264  tpostpos  6265  tposf12  6270  ercnv  6556  cnvct  6809  relcnvfi  6940  fsumcnv  11445  fisumcom2  11446  fprodcnv  11633  fprodcom2fi  11634