Metamath Proof Explorer


Theorem iunxunpr

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

Ref Expression
Hypotheses iunxunsn.1 x = X B = C
iunxunpr.2 x = Y B = D
Assertion iunxunpr X V Y W x A X Y B = x A B C D

Proof

Step Hyp Ref Expression
1 iunxunsn.1 x = X B = C
2 iunxunpr.2 x = Y B = D
3 iunxun x A X Y B = x A B x X Y B
4 1 2 iunxprg X V Y W x X Y B = C D
5 4 uneq2d X V Y W x A B x X Y B = x A B C D
6 3 5 syl5eq X V Y W x A X Y B = x A B C D