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 ⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝐷 )
iunxprg.2 ⊢ ( 𝑥 = 𝐵 → 𝐶 = 𝐸 )
Assertion iunxprg ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∪ 𝑥 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 ∪ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 iunxprg.1 ⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝐷 )
2 iunxprg.2 ⊢ ( 𝑥 = 𝐵 → 𝐶 = 𝐸 )
3 df-pr ⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
4 iuneq1 ⊢ ( { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } ) → ∪ 𝑥 ∈ { 𝐴 , 𝐵 } 𝐶 = ∪ 𝑥 ∈ ( { 𝐴 } ∪ { 𝐵 } ) 𝐶 )
5 3 4 ax-mp ⊢ ∪ 𝑥 ∈ { 𝐴 , 𝐵 } 𝐶 = ∪ 𝑥 ∈ ( { 𝐴 } ∪ { 𝐵 } ) 𝐶
6 iunxun ⊢ ∪ 𝑥 ∈ ( { 𝐴 } ∪ { 𝐵 } ) 𝐶 = ( ∪ 𝑥 ∈ { 𝐴 } 𝐶 ∪ ∪ 𝑥 ∈ { 𝐵 } 𝐶 )
7 5 6 eqtri ⊢ ∪ 𝑥 ∈ { 𝐴 , 𝐵 } 𝐶 = ( ∪ 𝑥 ∈ { 𝐴 } 𝐶 ∪ ∪ 𝑥 ∈ { 𝐵 } 𝐶 )
8 1 iunxsng ⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ { 𝐴 } 𝐶 = 𝐷 )
9 8 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∪ 𝑥 ∈ { 𝐴 } 𝐶 = 𝐷 )
10 2 iunxsng ⊢ ( 𝐵 ∈ 𝑊 → ∪ 𝑥 ∈ { 𝐵 } 𝐶 = 𝐸 )
11 10 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∪ 𝑥 ∈ { 𝐵 } 𝐶 = 𝐸 )
12 9 11 uneq12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∪ 𝑥 ∈ { 𝐴 } 𝐶 ∪ ∪ 𝑥 ∈ { 𝐵 } 𝐶 ) = ( 𝐷 ∪ 𝐸 ) )
13 7 12 eqtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∪ 𝑥 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 ∪ 𝐸 ) )