This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iinssd

Description: Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses iinssd.1 ⊢ φ → X ∈ A
iinssd.2 ⊢ x = X → B = D
iinssd.3 ⊢ φ → D ⊆ C
Assertion iinssd ⊢ φ → ⋂ x ∈ A B ⊆ C

Proof

Step Hyp Ref Expression
1 iinssd.1 ⊢ φ → X ∈ A
2 iinssd.2 ⊢ x = X → B = D
3 iinssd.3 ⊢ φ → D ⊆ C
4 2 sseq1d ⊢ x = X → B ⊆ C ↔ D ⊆ C
5 4 rspcev ⊢ X ∈ A ∧ D ⊆ C → ∃ x ∈ A B ⊆ C
6 1 3 5 syl2anc ⊢ φ → ∃ x ∈ A B ⊆ C
7 iinss ⊢ ∃ x ∈ A B ⊆ C → ⋂ x ∈ A B ⊆ C
8 6 7 syl ⊢ φ → ⋂ x ∈ A B ⊆ C