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