Theorem coundir 5509

Description: Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
coundir	|- ( ( A u. B ) o. C ) = ( ( A o. C ) u. ( B o. C ) )

Proof of Theorem coundir

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

Step	Hyp	Ref	Expression
1		unopab 4522	. . 3 |- ( { <. x , z >. | E. y ( x C y /\ y A z ) } u. { <. x , z >. | E. y ( x C y /\ y B z ) } ) = { <. x , z >. | ( E. y ( x C y /\ y A z ) \/ E. y ( x C y /\ y B z ) ) }
2		brun 4495	. . . . . . . 8 |- ( y ( A u. B ) z <-> ( y A z \/ y B z ) )
3	2	anbi2i 694	. . . . . . 7 |- ( ( x C y /\ y ( A u. B ) z ) <-> ( x C y /\ ( y A z \/ y B z ) ) )
4		andi 865	. . . . . . 7 |- ( ( x C y /\ ( y A z \/ y B z ) ) <-> ( ( x C y /\ y A z ) \/ ( x C y /\ y B z ) ) )
5	3, 4	bitri 249	. . . . . 6 |- ( ( x C y /\ y ( A u. B ) z ) <-> ( ( x C y /\ y A z ) \/ ( x C y /\ y B z ) ) )
6	5	exbii 1644	. . . . 5 |- ( E. y ( x C y /\ y ( A u. B ) z ) <-> E. y ( ( x C y /\ y A z ) \/ ( x C y /\ y B z ) ) )
7		19.43 1670	. . . . 5 |- ( E. y ( ( x C y /\ y A z ) \/ ( x C y /\ y B z ) ) <-> ( E. y ( x C y /\ y A z ) \/ E. y ( x C y /\ y B z ) ) )
8	6, 7	bitr2i 250	. . . 4 |- ( ( E. y ( x C y /\ y A z ) \/ E. y ( x C y /\ y B z ) ) <-> E. y ( x C y /\ y ( A u. B ) z ) )
9	8	opabbii 4511	. . 3 |- { <. x , z >. | ( E. y ( x C y /\ y A z ) \/ E. y ( x C y /\ y B z ) ) } = { <. x , z >. | E. y ( x C y /\ y ( A u. B ) z ) }
10	1, 9	eqtri 2496	. 2 |- ( { <. x , z >. | E. y ( x C y /\ y A z ) } u. { <. x , z >. | E. y ( x C y /\ y B z ) } ) = { <. x , z >. | E. y ( x C y /\ y ( A u. B ) z ) }
11		df-co 5008	. . 3 |- ( A o. C ) = { <. x , z >. | E. y ( x C y /\ y A z ) }
12		df-co 5008	. . 3 |- ( B o. C ) = { <. x , z >. | E. y ( x C y /\ y B z ) }
13	11, 12	uneq12i 3656	. 2 |- ( ( A o. C ) u. ( B o. C ) ) = ( { <. x , z >. | E. y ( x C y /\ y A z ) } u. { <. x , z >. | E. y ( x C y /\ y B z ) } )
14		df-co 5008	. 2 |- ( ( A u. B ) o. C ) = { <. x , z >. | E. y ( x C y /\ y ( A u. B ) z ) }
15	10, 13, 14	3eqtr4ri 2507	1 |- ( ( A u. B ) o. C ) = ( ( A o. C ) u. ( B o. C ) )

Syntax hints:   \/ wo 368   /\ wa 369   = wceq 1379   E.wex 1596   u. cun 3474   class class class wbr 4447   {copab 4504   o. ccom 5003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-br 4448  df-opab 4506  df-co 5008

This theorem is referenced by:  diophrw  30523  diophren  30578