Theorem iunxprg

Description: A pair index picks out two instances of an indexed union's argument. (Contributed by Alexander van der Vekens, 2-Feb-2018)

	Ref	Expression
Hypotheses	iunxprg.1	|- ( x = A -> C = D )
	iunxprg.2	|- ( x = B -> C = E )
Assertion	iunxprg	|- ( ( A e. V /\ B e. W ) -> U_ x e. { A , B } C = ( D u. E ) )

Proof

Step	Hyp	Ref	Expression
1		iunxprg.1	|- ( x = A -> C = D )
2		iunxprg.2	|- ( x = B -> C = E )
3		df-pr	|- { A , B } = ( { A } u. { B } )
4		iuneq1	|- ( { A , B } = ( { A } u. { B } ) -> U_ x e. { A , B } C = U_ x e. ( { A } u. { B } ) C )
5	3 4	ax-mp	|- U_ x e. { A , B } C = U_ x e. ( { A } u. { B } ) C
6		iunxun	|- U_ x e. ( { A } u. { B } ) C = ( U_ x e. { A } C u. U_ x e. { B } C )
7	5 6	eqtri	|- U_ x e. { A , B } C = ( U_ x e. { A } C u. U_ x e. { B } C )
8	1	iunxsng	|- ( A e. V -> U_ x e. { A } C = D )
9	8	adantr	|- ( ( A e. V /\ B e. W ) -> U_ x e. { A } C = D )
10	2	iunxsng	|- ( B e. W -> U_ x e. { B } C = E )
11	10	adantl	|- ( ( A e. V /\ B e. W ) -> U_ x e. { B } C = E )
12	9 11	uneq12d	|- ( ( A e. V /\ B e. W ) -> ( U_ x e. { A } C u. U_ x e. { B } C ) = ( D u. E ) )
13	7 12	syl5eq	|- ( ( A e. V /\ B e. W ) -> U_ x e. { A , B } C = ( D u. E ) )