Theorem iineqconst2

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

	Ref	Expression
Assertion	iineqconst2	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ∩ 𝑥 ∈ 𝐴 𝐵 = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		r19.2z	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝐵 = 𝐶 )
2		eqimss	⊢ ( 𝐵 = 𝐶 → 𝐵 ⊆ 𝐶 )
3	2	reximi	⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∃ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
4		iinss	⊢ ( ∃ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
5	1 3 4	3syl	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 )
6		eqimss2	⊢ ( 𝐵 = 𝐶 → 𝐶 ⊆ 𝐵 )
7	6	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 )
8	7	adantl	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 )
9		ssiin	⊢ ( 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ⊆ 𝐵 )
10	8 9	sylibr	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → 𝐶 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 )
11	5 10	eqssd	⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ∩ 𝑥 ∈ 𝐴 𝐵 = 𝐶 )