Metamath Proof Explorer

Theorem iunss1

Description: Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004) (Proof shortened by Andrew Salmon, 25-Jul-2011)

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

Proof

Step Hyp Ref Expression
1 ssrexv ⊢ A ⊆ B → ∃ x ∈ A y ∈ C → ∃ x ∈ B y ∈ C
2 eliun ⊢ y ∈ ⋃ x ∈ A C ↔ ∃ x ∈ A y ∈ C
3 eliun ⊢ y ∈ ⋃ x ∈ B C ↔ ∃ x ∈ B y ∈ C
4 1 2 3 3imtr4g ⊢ A ⊆ B → y ∈ ⋃ x ∈ A C → y ∈ ⋃ x ∈ B C
5 4 ssrdv ⊢ A ⊆ B → ⋃ x ∈ A C ⊆ ⋃ x ∈ B C