Metamath Proof Explorer


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 syl5eq ( 𝑋𝑉 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) 𝐵 = ( 𝑥𝐴 𝐵𝐶 ) )