Metamath Proof Explorer

Theorem iinssiin

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

Ref Expression
Hypotheses iinssiin.1 ⊢ Ⅎ x φ
iinssiin.2 ⊢ φ ∧ x ∈ A → B ⊆ C
Assertion iinssiin ⊢ φ → ⋂ x ∈ A B ⊆ ⋂ x ∈ A C

Proof

Step Hyp Ref Expression
1 iinssiin.1 ⊢ Ⅎ x φ
2 iinssiin.2 ⊢ φ ∧ x ∈ A → B ⊆ C
3 nfii1 ⊢ Ⅎ _ x ⋂ x ∈ A B
4 3 nfcri ⊢ Ⅎ x y ∈ ⋂ x ∈ A B
5 1 4 nfan ⊢ Ⅎ x φ ∧ y ∈ ⋂ x ∈ A B
6 2 adantlr ⊢ φ ∧ y ∈ ⋂ x ∈ A B ∧ x ∈ A → B ⊆ C
7 eliinid ⊢ y ∈ ⋂ x ∈ A B ∧ x ∈ A → y ∈ B
8 7 adantll ⊢ φ ∧ y ∈ ⋂ x ∈ A B ∧ x ∈ A → y ∈ B
9 6 8 sseldd ⊢ φ ∧ y ∈ ⋂ x ∈ A B ∧ x ∈ A → y ∈ C
10 9 ex ⊢ φ ∧ y ∈ ⋂ x ∈ A B → x ∈ A → y ∈ C
11 5 10 ralrimi ⊢ φ ∧ y ∈ ⋂ x ∈ A B → ∀ x ∈ A y ∈ C
12 eliin ⊢ y ∈ V → y ∈ ⋂ x ∈ A C ↔ ∀ x ∈ A y ∈ C
13 12 elv ⊢ y ∈ ⋂ x ∈ A C ↔ ∀ x ∈ A y ∈ C
14 11 13 sylibr ⊢ φ ∧ y ∈ ⋂ x ∈ A B → y ∈ ⋂ x ∈ A C
15 14 ssd ⊢ φ → ⋂ x ∈ A B ⊆ ⋂ x ∈ A C