This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssiun2s

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

Ref Expression
Hypothesis ssiun2s.1 ⊢ x = C → B = D
Assertion ssiun2s ⊢ C ∈ A → D ⊆ ⋃ x ∈ A B

Proof

Step Hyp Ref Expression
1 ssiun2s.1 ⊢ x = C → B = D
2 nfcv ⊢ Ⅎ _ x C
3 nfcv ⊢ Ⅎ _ x D
4 nfiu1 ⊢ Ⅎ _ x ⋃ x ∈ A B
5 3 4 nfss ⊢ Ⅎ x D ⊆ ⋃ x ∈ A B
6 1 sseq1d ⊢ x = C → B ⊆ ⋃ x ∈ A B ↔ D ⊆ ⋃ x ∈ A B
7 ssiun2 ⊢ x ∈ A → B ⊆ ⋃ x ∈ A B
8 2 5 6 7 vtoclgaf ⊢ C ∈ A → D ⊆ ⋃ x ∈ A B