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 ) ) |
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 ) ) |