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 e. V /\ Y e. W ) -> U_ x e. ( A u. { X , Y } ) B = ( U_ x e. A B u. ( C u. D ) ) )

Proof

Step	Hyp	Ref	Expression
1		iunxunsn.1	|- ( x = X -> B = C )
2		iunxunpr.2	|- ( x = Y -> B = D )
3		iunxun	|- U_ x e. ( A u. { X , Y } ) B = ( U_ x e. A B u. U_ x e. { X , Y } B )
4	1 2	iunxprg	|- ( ( X e. V /\ Y e. W ) -> U_ x e. { X , Y } B = ( C u. D ) )
5	4	uneq2d	|- ( ( X e. V /\ Y e. W ) -> ( U_ x e. A B u. U_ x e. { X , Y } B ) = ( U_ x e. A B u. ( C u. D ) ) )
6	3 5	syl5eq	|- ( ( X e. V /\ Y e. W ) -> U_ x e. ( A u. { X , Y } ) B = ( U_ x e. A B u. ( C u. D ) ) )