Theorem cnvco 5039

Description: Distributive law of converse over class composition. Theorem 26 of [Suppes] p. 64. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
cnvco	|- `' ( A o. B ) = ( `' B o. `' A )

Proof of Theorem cnvco

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

Step	Hyp	Ref	Expression
1		exancom 1733	. . . 4 |- ( E. z ( x B z /\ z A y ) <-> E. z ( z A y /\ x B z ) )
2		vex 3060	. . . . 5 |- x e. _V
3		vex 3060	. . . . 5 |- y e. _V
4	2, 3	brco 5024	. . . 4 |- ( x ( A o. B ) y <-> E. z ( x B z /\ z A y ) )
5		vex 3060	. . . . . . 7 |- z e. _V
6	3, 5	brcnv 5036	. . . . . 6 |- ( y `' A z <-> z A y )
7	5, 2	brcnv 5036	. . . . . 6 |- ( z `' B x <-> x B z )
8	6, 7	anbi12i 708	. . . . 5 |- ( ( y `' A z /\ z `' B x ) <-> ( z A y /\ x B z ) )
9	8	exbii 1729	. . . 4 |- ( E. z ( y `' A z /\ z `' B x ) <-> E. z ( z A y /\ x B z ) )
10	1, 4, 9	3bitr4i 285	. . 3 |- ( x ( A o. B ) y <-> E. z ( y `' A z /\ z `' B x ) )
11	10	opabbii 4481	. 2 |- { <. y , x >. | x ( A o. B ) y } = { <. y , x >. | E. z ( y `' A z /\ z `' B x ) }
12		df-cnv 4861	. 2 |- `' ( A o. B ) = { <. y , x >. | x ( A o. B ) y }
13		df-co 4862	. 2 |- ( `' B o. `' A ) = { <. y , x >. | E. z ( y `' A z /\ z `' B x ) }
14	11, 12, 13	3eqtr4i 2494	1 |- `' ( A o. B ) = ( `' B o. `' A )

Syntax hints:   /\ wa 375   = wceq 1455   E.wex 1674   class class class wbr 4416   {copab 4474   `'ccnv 4852   o. ccom 4857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417  df-opab 4476  df-cnv 4861  df-co 4862

This theorem is referenced by:  rncoss  5114  rncoeq  5117  dmco  5362  cores2  5367  co01  5369  coi2  5371  relcnvtr  5374  dfdm2  5387  f1co  5811  cofunex2g  6785  fparlem3  6925  fparlem4  6926  supp0cosupp0  6981  imacosupp  6982  fsuppcolem  7940  relexpcnv  13147  relexpaddg  13165  cnvps  16507  gimco  16981  gsumzf1o  17595  cnco  20331  ptrescn  20703  qtopcn  20778  hmeoco  20836  cncombf  22663  deg1val  23094  fcoinver  28263  ofpreima  28317  mbfmco  29135  eulerpartlemmf  29257  cvmliftmolem1  30053  cvmlift2lem9a  30075  cvmlift2lem9  30083  mclsppslem  30270  ftc1anclem3  32064  trlcocnv  34332  tendoicl  34408  cdlemk45  34559  cononrel1  36245  cononrel2  36246  cnvtrcl0  36278  cnvtrrel  36307  relexpaddss  36355  frege131d  36401