Theorem iunxunpr

Description: Appending two sets to an indexed union. (Contributed by Thierry Arnoux, 20-Nov-2023)

	Ref	Expression
Hypotheses	iunxunsn.1	⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐶 )
	iunxunpr.2	⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐷 )
Assertion	iunxunpr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ∪ 𝑥 ∈ ( 𝐴 ∪ { 𝑋 , 𝑌 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ ( 𝐶 ∪ 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iunxunsn.1	⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐶 )
2		iunxunpr.2	⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐷 )
3		iunxun	⊢ ∪ 𝑥 ∈ ( 𝐴 ∪ { 𝑋 , 𝑌 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ ∪ 𝑥 ∈ { 𝑋 , 𝑌 } 𝐵 )
4	1 2	iunxprg	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ∪ 𝑥 ∈ { 𝑋 , 𝑌 } 𝐵 = ( 𝐶 ∪ 𝐷 ) )
5	4	uneq2d	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ ∪ 𝑥 ∈ { 𝑋 , 𝑌 } 𝐵 ) = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ ( 𝐶 ∪ 𝐷 ) ) )
6	3 5	syl5eq	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ∪ 𝑥 ∈ ( 𝐴 ∪ { 𝑋 , 𝑌 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ ( 𝐶 ∪ 𝐷 ) ) )