Theorem ssiun2s

Description: Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003)

	Ref	Expression
Hypothesis	ssiun2s.1	⊢ ( 𝑥 = 𝐶 → 𝐵 = 𝐷 )
Assertion	ssiun2s	⊢ ( 𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ssiun2s.1	⊢ ( 𝑥 = 𝐶 → 𝐵 = 𝐷 )
2		nfcv	⊢ Ⅎ 𝑥 𝐶
3		nfcv	⊢ Ⅎ 𝑥 𝐷
4		nfiu1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵
5	3 4	nfss	⊢ Ⅎ 𝑥 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
6	1	sseq1d	⊢ ( 𝑥 = 𝐶 → ( 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
7		ssiun2	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
8	2 5 6 7	vtoclgaf	⊢ ( 𝐶 ∈ 𝐴 → 𝐷 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )