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

Metamath Proof Explorer

Theorem ssiun2sf

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

Ref Expression
Hypotheses ssiun2sf.1 ⊢ Ⅎ _ x A
ssiun2sf.2 ⊢ Ⅎ _ x C
ssiun2sf.3 ⊢ Ⅎ _ x D
ssiun2sf.4 ⊢ x = C → B = D
Assertion ssiun2sf ⊢ C ∈ A → D ⊆ ⋃ x ∈ A B

Proof

Step Hyp Ref Expression
1 ssiun2sf.1 ⊢ Ⅎ _ x A
2 ssiun2sf.2 ⊢ Ⅎ _ x C
3 ssiun2sf.3 ⊢ Ⅎ _ x D
4 ssiun2sf.4 ⊢ x = C → B = D
5 2 1 nfel ⊢ Ⅎ x C ∈ A
6 nfiu1 ⊢ Ⅎ _ x ⋃ x ∈ A B
7 3 6 nfss ⊢ Ⅎ x D ⊆ ⋃ x ∈ A B
8 5 7 nfim ⊢ Ⅎ x C ∈ A → D ⊆ ⋃ x ∈ A B
9 eleq1 ⊢ x = C → x ∈ A ↔ C ∈ A
10 4 sseq1d ⊢ x = C → B ⊆ ⋃ x ∈ A B ↔ D ⊆ ⋃ x ∈ A B
11 9 10 imbi12d ⊢ x = C → x ∈ A → B ⊆ ⋃ x ∈ A B ↔ C ∈ A → D ⊆ ⋃ x ∈ A B
12 ssiun2 ⊢ x ∈ A → B ⊆ ⋃ x ∈ A B
13 2 8 11 12 vtoclgf ⊢ C ∈ A → C ∈ A → D ⊆ ⋃ x ∈ A B
14 13 pm2.43i ⊢ C ∈ A → D ⊆ ⋃ x ∈ A B