Metamath Proof Explorer

Theorem coundi

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

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

Proof

Step Hyp Ref Expression
1 unopab 
 |-  ( { <. x , y >. | E. z ( x B z /\ z A y ) } u. { <. x , y >. | E. z ( x C z /\ z A y ) } ) = { <. x , y >. | ( E. z ( x B z /\ z A y ) \/ E. z ( x C z /\ z A y ) ) }
2 brun 
 |-  ( x ( B u. C ) z <-> ( x B z \/ x C z ) )
3 2 anbi1i 
 |-  ( ( x ( B u. C ) z /\ z A y ) <-> ( ( x B z \/ x C z ) /\ z A y ) )
4 andir 
 |-  ( ( ( x B z \/ x C z ) /\ z A y ) <-> ( ( x B z /\ z A y ) \/ ( x C z /\ z A y ) ) )
5 3 4 bitri 
 |-  ( ( x ( B u. C ) z /\ z A y ) <-> ( ( x B z /\ z A y ) \/ ( x C z /\ z A y ) ) )
6 5 exbii 
 |-  ( E. z ( x ( B u. C ) z /\ z A y ) <-> E. z ( ( x B z /\ z A y ) \/ ( x C z /\ z A y ) ) )
7 19.43 
 |-  ( E. z ( ( x B z /\ z A y ) \/ ( x C z /\ z A y ) ) <-> ( E. z ( x B z /\ z A y ) \/ E. z ( x C z /\ z A y ) ) )
8 6 7 bitr2i 
 |-  ( ( E. z ( x B z /\ z A y ) \/ E. z ( x C z /\ z A y ) ) <-> E. z ( x ( B u. C ) z /\ z A y ) )
9 8 opabbii 
 |-  { <. x , y >. | ( E. z ( x B z /\ z A y ) \/ E. z ( x C z /\ z A y ) ) } = { <. x , y >. | E. z ( x ( B u. C ) z /\ z A y ) }
10 1 9 eqtri 
 |-  ( { <. x , y >. | E. z ( x B z /\ z A y ) } u. { <. x , y >. | E. z ( x C z /\ z A y ) } ) = { <. x , y >. | E. z ( x ( B u. C ) z /\ z A y ) }
11 df-co 
 |-  ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
12 df-co 
 |-  ( A o. C ) = { <. x , y >. | E. z ( x C z /\ z A y ) }
13 11 12 uneq12i 
 |-  ( ( A o. B ) u. ( A o. C ) ) = ( { <. x , y >. | E. z ( x B z /\ z A y ) } u. { <. x , y >. | E. z ( x C z /\ z A y ) } )
14 df-co 
 |-  ( A o. ( B u. C ) ) = { <. x , y >. | E. z ( x ( B u. C ) z /\ z A y ) }
15 10 13 14 3eqtr4ri 
 |-  ( A o. ( B u. C ) ) = ( ( A o. B ) u. ( A o. C ) )