Metamath Proof Explorer

Theorem ssiinf

Description: Subset theorem for an indexed intersection. (Contributed by FL, 15-Oct-2012) (Proof shortened by Mario Carneiro, 14-Oct-2016)

Ref Expression
Hypothesis ssiinf.1 ⊢ Ⅎ _ x C
Assertion ssiinf ⊢ C ⊆ ⋂ x ∈ A B ↔ ∀ x ∈ A C ⊆ B

Proof

Step Hyp Ref Expression
1 ssiinf.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 3 ralbii ⊢ ∀ y ∈ C y ∈ ⋂ x ∈ A B ↔ ∀ y ∈ C ∀ x ∈ A y ∈ B
5 nfcv ⊢ Ⅎ _ y A
6 1 5 ralcomf ⊢ ∀ y ∈ C ∀ x ∈ A y ∈ B ↔ ∀ x ∈ A ∀ y ∈ C y ∈ B
7 4 6 bitri ⊢ ∀ y ∈ C y ∈ ⋂ x ∈ A B ↔ ∀ x ∈ A ∀ y ∈ C y ∈ B
8 dfss3 ⊢ C ⊆ ⋂ x ∈ A B ↔ ∀ y ∈ C y ∈ ⋂ x ∈ A B
9 dfss3 ⊢ C ⊆ B ↔ ∀ y ∈ C y ∈ B
10 9 ralbii ⊢ ∀ x ∈ A C ⊆ B ↔ ∀ x ∈ A ∀ y ∈ C y ∈ B
11 7 8 10 3bitr4i ⊢ C ⊆ ⋂ x ∈ A B ↔ ∀ x ∈ A C ⊆ B