Metamath Proof Explorer

Theorem coundir

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

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

Proof

Step Hyp Ref Expression
1 unopab 
 |-  ( { <. 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 
 |-  ( y ( A u. B ) z <-> ( y A z \/ y B z ) )
3 2 anbi2i 
 |-  ( ( x C y /\ y ( A u. B ) z ) <-> ( x C y /\ ( y A z \/ y B z ) ) )
4 andi 
 |-  ( ( 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 
 |-  ( ( x C y /\ y ( A u. B ) z ) <-> ( ( x C y /\ y A z ) \/ ( x C y /\ y B z ) ) )
6 5 exbii 
 |-  ( 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 
 |-  ( 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 
 |-  ( ( 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 
 |-  { <. 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 
 |-  ( { <. 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 
 |-  ( A o. C ) = { <. x , z >. | E. y ( x C y /\ y A z ) }
12 df-co 
 |-  ( B o. C ) = { <. x , z >. | E. y ( x C y /\ y B z ) }
13 11 12 uneq12i 
 |-  ( ( 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 
 |-  ( ( A u. B ) o. C ) = { <. x , z >. | E. y ( x C y /\ y ( A u. B ) z ) }
15 10 13 14 3eqtr4ri 
 |-  ( ( A u. B ) o. C ) = ( ( A o. C ) u. ( B o. C ) )