Metamath Proof Explorer

Theorem iinss1

Description: Subclass theorem for indexed intersection. (Contributed by NM, 24-Jan-2012)

Ref Expression
Assertion iinss1 ⊢ A ⊆ B → ⋂ x ∈ B C ⊆ ⋂ x ∈ A C

Proof

Step Hyp Ref Expression
1 ssralv ⊢ A ⊆ B → ∀ x ∈ B y ∈ C → ∀ x ∈ A y ∈ C
2 eliin ⊢ y ∈ V → y ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B y ∈ C
3 2 elv ⊢ y ∈ ⋂ x ∈ B C ↔ ∀ x ∈ B y ∈ C
4 eliin ⊢ y ∈ V → y ∈ ⋂ x ∈ A C ↔ ∀ x ∈ A y ∈ C
5 4 elv ⊢ y ∈ ⋂ x ∈ A C ↔ ∀ x ∈ A y ∈ C
6 1 3 5 3imtr4g ⊢ A ⊆ B → y ∈ ⋂ x ∈ B C → y ∈ ⋂ x ∈ A C
7 6 ssrdv ⊢ A ⊆ B → ⋂ x ∈ B C ⊆ ⋂ x ∈ A C