This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 ) → ∩ 𝑥 ∈ 𝐴 𝐵 = 𝐶 )