Theorem cnvco 5136

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 1639	. . . 4 |- ( E. z ( x B z /\ z A y ) <-> E. z ( z A y /\ x B z ) )
2		vex 3081	. . . . 5 |- x e. _V
3		vex 3081	. . . . 5 |- y e. _V
4	2, 3	brco 5121	. . . 4 |- ( x ( A o. B ) y <-> E. z ( x B z /\ z A y ) )
5		vex 3081	. . . . . . 7 |- z e. _V
6	3, 5	brcnv 5133	. . . . . 6 |- ( y `' A z <-> z A y )
7	5, 2	brcnv 5133	. . . . . 6 |- ( z `' B x <-> x B z )
8	6, 7	anbi12i 697	. . . . 5 |- ( ( y `' A z /\ z `' B x ) <-> ( z A y /\ x B z ) )
9	8	exbii 1635	. . . 4 |- ( E. z ( y `' A z /\ z `' B x ) <-> E. z ( z A y /\ x B z ) )
10	1, 4, 9	3bitr4i 277	. . 3 |- ( x ( A o. B ) y <-> E. z ( y `' A z /\ z `' B x ) )
11	10	opabbii 4467	. 2 |- { <. y , x >. | x ( A o. B ) y } = { <. y , x >. | E. z ( y `' A z /\ z `' B x ) }
12		df-cnv 4959	. 2 |- `' ( A o. B ) = { <. y , x >. | x ( A o. B ) y }
13		df-co 4960	. 2 |- ( `' B o. `' A ) = { <. y , x >. | E. z ( y `' A z /\ z `' B x ) }
14	11, 12, 13	3eqtr4i 2493	1 |- `' ( A o. B ) = ( `' B o. `' A )

Syntax hints:   /\ wa 369   = wceq 1370   E.wex 1587   class class class wbr 4403   {copab 4460   `'ccnv 4950   o. ccom 4955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-rab 2808  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-br 4404  df-opab 4462  df-cnv 4959  df-co 4960

This theorem is referenced by:  rncoss  5211  rncoeq  5214  dmco  5457  cores2  5461  co01  5463  coi2  5465  relcnvtr  5468  dfdm2  5480  f1co  5726  cofunex2g  6655  fparlem3  6787  fparlem4  6788  supp0cosupp0  6841  imacosupp  6842  fsuppcolem  7764  mapfienOLD  8041  cnvps  15504  gimco  15918  gsumval3OLD  16506  gsumzf1o  16515  gsumzf1oOLD  16518  cnco  19005  ptrescn  19347  qtopcn  19422  hmeoco  19480  cncombf  21272  deg1val  21703  deg1valOLD  21704  ofpreima  26155  mbfmco  26843  eulerpartlemmf  26922  cvmliftmolem1  27334  cvmlift2lem9a  27356  cvmlift2lem9  27364  relexpcnv  27499  ftc1anclem3  28637  trlcocnv  34722  tendoicl  34798  cdlemk45  34949