This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iunxprg

Description: A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018)

Ref Expression
Hypotheses iunxprg.1 
|- ( x = A -> C = D )
iunxprg.2 
|- ( x = B -> C = E )
Assertion iunxprg 
|- ( ( A e. V /\ B e. W ) -> U_ x e. { A , B } C = ( D u. E ) )

Proof

Step Hyp Ref Expression
1 iunxprg.1 
 |-  ( x = A -> C = D )
2 iunxprg.2 
 |-  ( x = B -> C = E )
3 df-pr 
 |-  { A , B } = ( { A } u. { B } )
4 iuneq1 
 |-  ( { A , B } = ( { A } u. { B } ) -> U_ x e. { A , B } C = U_ x e. ( { A } u. { B } ) C )
5 3 4 ax-mp 
 |-  U_ x e. { A , B } C = U_ x e. ( { A } u. { B } ) C
6 iunxun 
 |-  U_ x e. ( { A } u. { B } ) C = ( U_ x e. { A } C u. U_ x e. { B } C )
7 5 6 eqtri 
 |-  U_ x e. { A , B } C = ( U_ x e. { A } C u. U_ x e. { B } C )
8 1 iunxsng 
 |-  ( A e. V -> U_ x e. { A } C = D )
9 8 adantr 
 |-  ( ( A e. V /\ B e. W ) -> U_ x e. { A } C = D )
10 2 iunxsng 
 |-  ( B e. W -> U_ x e. { B } C = E )
11 10 adantl 
 |-  ( ( A e. V /\ B e. W ) -> U_ x e. { B } C = E )
12 9 11 uneq12d 
 |-  ( ( A e. V /\ B e. W ) -> ( U_ x e. { A } C u. U_ x e. { B } C ) = ( D u. E ) )
13 7 12 eqtrid 
 |-  ( ( A e. V /\ B e. W ) -> U_ x e. { A , B } C = ( D u. E ) )