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 e. V -> U_ x e. ( A u. { X } ) B = ( U_ x e. A B u. C ) )

Proof

Step Hyp Ref Expression
1 iunxunsn.1
 |-  ( x = X -> B = C )
2 iunxun
 |-  U_ x e. ( A u. { X } ) B = ( U_ x e. A B u. U_ x e. { X } B )
3 1 iunxsng
 |-  ( X e. V -> U_ x e. { X } B = C )
4 3 uneq2d
 |-  ( X e. V -> ( U_ x e. A B u. U_ x e. { X } B ) = ( U_ x e. A B u. C ) )
5 2 4 syl5eq
 |-  ( X e. V -> U_ x e. ( A u. { X } ) B = ( U_ x e. A B u. C ) )