Metamath Proof Explorer

Theorem iinss1

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

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

Proof

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