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