Theorem iunxunsn

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

	Ref	Expression
Hypothesis	iunxunsn.1	⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐶 )
Assertion	iunxunsn	⊢ ( 𝑋 ∈ 𝑉 → ∪ 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		iunxunsn.1	⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐶 )
2		iunxun	⊢ ∪ 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ ∪ 𝑥 ∈ { 𝑋 } 𝐵 )
3	1	iunxsng	⊢ ( 𝑋 ∈ 𝑉 → ∪ 𝑥 ∈ { 𝑋 } 𝐵 = 𝐶 )
4	3	uneq2d	⊢ ( 𝑋 ∈ 𝑉 → ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ ∪ 𝑥 ∈ { 𝑋 } 𝐵 ) = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶 ) )
5	2 4	eqtrid	⊢ ( 𝑋 ∈ 𝑉 → ∪ 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶 ) )