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 x = X B = C
Assertion iunxunsn X V x A X B = x A B C

Proof

Step Hyp Ref Expression
1 iunxunsn.1 x = X B = C
2 iunxun x A X B = x A B x X B
3 1 iunxsng X V x X B = C
4 3 uneq2d X V x A B x X B = x A B C
5 2 4 syl5eq X V x A X B = x A B C