Theorem ssiun2sf

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

	Ref	Expression
Hypotheses	ssiun2sf.1	⊢ Ⅎ 𝑥 𝐴
	ssiun2sf.2	⊢ Ⅎ 𝑥 𝐶
	ssiun2sf.3	⊢ Ⅎ 𝑥 𝐷
	ssiun2sf.4	⊢ ( 𝑥 = 𝐶 → 𝐵 = 𝐷 )
Assertion	ssiun2sf	⊢ ( 𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ssiun2sf.1	⊢ Ⅎ 𝑥 𝐴
2		ssiun2sf.2	⊢ Ⅎ 𝑥 𝐶
3		ssiun2sf.3	⊢ Ⅎ 𝑥 𝐷
4		ssiun2sf.4	⊢ ( 𝑥 = 𝐶 → 𝐵 = 𝐷 )
5	2 1	nfel	⊢ Ⅎ 𝑥 𝐶 ∈ 𝐴
6		nfiu1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵
7	3 6	nfss	⊢ Ⅎ 𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
8	5 7	nfim	⊢ Ⅎ 𝑥 ( 𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
9		eleq1	⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
10	4	sseq1d	⊢ ( 𝑥 = 𝐶 → ( 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
11	9 10	imbi12d	⊢ ( 𝑥 = 𝐶 → ( ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) )
12		ssiun2	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
13	2 8 11 12	vtoclgf	⊢ ( 𝐶 ∈ 𝐴 → ( 𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
14	13	pm2.43i	⊢ ( 𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )