Metamath Proof Explorer

Theorem ss2iun

Description: Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion ss2iun ⊢ ∀ x ∈ A B ⊆ C → ⋃ x ∈ A B ⊆ ⋃ x ∈ A C

Proof

Step Hyp Ref Expression
1 ssel ⊢ B ⊆ C → y ∈ B → y ∈ C
2 1 ralimi ⊢ ∀ x ∈ A B ⊆ C → ∀ x ∈ A y ∈ B → y ∈ C
3 rexim ⊢ ∀ x ∈ A y ∈ B → y ∈ C → ∃ x ∈ A y ∈ B → ∃ x ∈ A y ∈ C
4 2 3 syl ⊢ ∀ x ∈ A B ⊆ C → ∃ x ∈ A y ∈ B → ∃ x ∈ A y ∈ C
5 eliun ⊢ y ∈ ⋃ x ∈ A B ↔ ∃ x ∈ A y ∈ B
6 eliun ⊢ y ∈ ⋃ x ∈ A C ↔ ∃ x ∈ A y ∈ C
7 4 5 6 3imtr4g ⊢ ∀ x ∈ A B ⊆ C → y ∈ ⋃ x ∈ A B → y ∈ ⋃ x ∈ A C
8 7 ssrdv ⊢ ∀ x ∈ A B ⊆ C → ⋃ x ∈ A B ⊆ ⋃ x ∈ A C