Metamath Proof Explorer

Theorem iineqconst2

Description: Indexed intersection of identical classes. (Contributed by Zhi Wang, 6-Nov-2025)

Ref Expression
Assertion iineqconst2 ⊢ A ≠ ∅ ∧ ∀ x ∈ A B = C → ⋂ x ∈ A B = C

Proof

Step Hyp Ref Expression
1 r19.2z ⊢ A ≠ ∅ ∧ ∀ x ∈ A B = C → ∃ x ∈ A B = C
2 eqimss ⊢ B = C → B ⊆ C
3 2 reximi ⊢ ∃ x ∈ A B = C → ∃ x ∈ A B ⊆ C
4 iinss ⊢ ∃ x ∈ A B ⊆ C → ⋂ x ∈ A B ⊆ C
5 1 3 4 3syl ⊢ A ≠ ∅ ∧ ∀ x ∈ A B = C → ⋂ x ∈ A B ⊆ C
6 eqimss2 ⊢ B = C → C ⊆ B
7 6 ralimi ⊢ ∀ x ∈ A B = C → ∀ x ∈ A C ⊆ B
8 7 adantl ⊢ A ≠ ∅ ∧ ∀ x ∈ A B = C → ∀ x ∈ A C ⊆ B
9 ssiin ⊢ C ⊆ ⋂ x ∈ A B ↔ ∀ x ∈ A C ⊆ B
10 8 9 sylibr ⊢ A ≠ ∅ ∧ ∀ x ∈ A B = C → C ⊆ ⋂ x ∈ A B
11 5 10 eqssd ⊢ A ≠ ∅ ∧ ∀ x ∈ A B = C → ⋂ x ∈ A B = C