Metamath Proof Explorer

Theorem iinssf

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

Ref Expression
Hypothesis iinssf.1 ⊢ Ⅎ _ x C
Assertion iinssf ⊢ ∃ x ∈ A B ⊆ C → ⋂ x ∈ A B ⊆ C

Proof

Step Hyp Ref Expression
1 iinssf.1 ⊢ Ⅎ _ x C
2 eliin ⊢ y ∈ V → y ∈ ⋂ x ∈ A B ↔ ∀ x ∈ A y ∈ B
3 2 elv ⊢ y ∈ ⋂ x ∈ A B ↔ ∀ x ∈ A y ∈ B
4 ssel ⊢ B ⊆ C → y ∈ B → y ∈ C
5 4 reximi ⊢ ∃ x ∈ A B ⊆ C → ∃ x ∈ A y ∈ B → y ∈ C
6 1 nfcri ⊢ Ⅎ x y ∈ C
7 6 r19.36vf ⊢ ∃ x ∈ A y ∈ B → y ∈ C → ∀ x ∈ A y ∈ B → y ∈ C
8 5 7 syl ⊢ ∃ x ∈ A B ⊆ C → ∀ x ∈ A y ∈ B → y ∈ C
9 3 8 syl5bi ⊢ ∃ x ∈ A B ⊆ C → y ∈ ⋂ x ∈ A B → y ∈ C
10 9 ssrdv ⊢ ∃ x ∈ A B ⊆ C → ⋂ x ∈ A B ⊆ C