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

Metamath Proof Explorer

Theorem iinssdf

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

Ref Expression
Hypotheses iinssdf.a ⊢ Ⅎ _ x A
iinssdf.n ⊢ Ⅎ _ x X
iinssdf.c ⊢ Ⅎ _ x C
iinssdf.d ⊢ Ⅎ _ x D
iinssdf.x ⊢ φ → X ∈ A
iinssdf.b ⊢ x = X → B = D
iinssdf.s ⊢ φ → D ⊆ C
Assertion iinssdf ⊢ φ → ⋂ x ∈ A B ⊆ C

Proof

Step Hyp Ref Expression
1 iinssdf.a ⊢ Ⅎ _ x A
2 iinssdf.n ⊢ Ⅎ _ x X
3 iinssdf.c ⊢ Ⅎ _ x C
4 iinssdf.d ⊢ Ⅎ _ x D
5 iinssdf.x ⊢ φ → X ∈ A
6 iinssdf.b ⊢ x = X → B = D
7 iinssdf.s ⊢ φ → D ⊆ C
8 4 3 nfss ⊢ Ⅎ x D ⊆ C
9 6 sseq1d ⊢ x = X → B ⊆ C ↔ D ⊆ C
10 8 2 1 9 rspcef ⊢ X ∈ A ∧ D ⊆ C → ∃ x ∈ A B ⊆ C
11 5 7 10 syl2anc ⊢ φ → ∃ x ∈ A B ⊆ C
12 3 iinssf ⊢ ∃ x ∈ A B ⊆ C → ⋂ x ∈ A B ⊆ C
13 11 12 syl ⊢ φ → ⋂ x ∈ A B ⊆ C