Metamath Proof Explorer

Theorem iinss2

Description: An indexed intersection is included in any of its members. (Contributed by FL, 15-Oct-2012)

Ref Expression
Assertion iinss2 ⊢ x ∈ A → ⋂ x ∈ A B ⊆ B

Proof

Step Hyp Ref Expression
1 eliin ⊢ y ∈ V → y ∈ ⋂ x ∈ A B ↔ ∀ x ∈ A y ∈ B
2 1 elv ⊢ y ∈ ⋂ x ∈ A B ↔ ∀ x ∈ A y ∈ B
3 rsp ⊢ ∀ x ∈ A y ∈ B → x ∈ A → y ∈ B
4 3 com12 ⊢ x ∈ A → ∀ x ∈ A y ∈ B → y ∈ B
5 2 4 biimtrid ⊢ x ∈ A → y ∈ ⋂ x ∈ A B → y ∈ B
6 5 ssrdv ⊢ x ∈ A → ⋂ x ∈ A B ⊆ B