Theorem ssiun2sf

Description: Subset relationship for an indexed union. (Contributed by Thierry Arnoux, 31-Dec-2016)

	Ref	Expression
Hypotheses	ssiun2sf.1	|- F/_ x A
	ssiun2sf.2	|- F/_ x C
	ssiun2sf.3	|- F/_ x D
	ssiun2sf.4	|- ( x = C -> B = D )
Assertion	ssiun2sf	|- ( C e. A -> D C_ U_ x e. A B )

Proof

Step	Hyp	Ref	Expression
1		ssiun2sf.1	|- F/_ x A
2		ssiun2sf.2	|- F/_ x C
3		ssiun2sf.3	|- F/_ x D
4		ssiun2sf.4	|- ( x = C -> B = D )
5	2 1	nfel	|- F/ x C e. A
6		nfiu1	|- F/_ x U_ x e. A B
7	3 6	nfss	|- F/ x D C_ U_ x e. A B
8	5 7	nfim	|- F/ x ( C e. A -> D C_ U_ x e. A B )
9		eleq1	|- ( x = C -> ( x e. A <-> C e. A ) )
10	4	sseq1d	|- ( x = C -> ( B C_ U_ x e. A B <-> D C_ U_ x e. A B ) )
11	9 10	imbi12d	|- ( x = C -> ( ( x e. A -> B C_ U_ x e. A B ) <-> ( C e. A -> D C_ U_ x e. A B ) ) )
12		ssiun2	|- ( x e. A -> B C_ U_ x e. A B )
13	2 8 11 12	vtoclgf	|- ( C e. A -> ( C e. A -> D C_ U_ x e. A B ) )
14	13	pm2.43i	|- ( C e. A -> D C_ U_ x e. A B )