iineqconst2

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

		Ref	Expression
	Assertion	iineqconst2	$⊢ (A \neq \emptyset \land \forall x \in A B = C) \to ⋂_{x \in A} B = C$

Step	Hyp	Ref	Expression
1		r19.2z	$⊢ (A \neq \emptyset \land \forall x \in A B = C) \to \exists x \in A B = C$
2		eqimss	$⊢ B = C \to B \subseteq C$
3	2	reximi	$⊢ \exists x \in A B = C \to \exists x \in A B \subseteq C$
4		iinss	$⊢ \exists x \in A B \subseteq C \to ⋂_{x \in A} B \subseteq C$
5	1 3 4	3syl	$⊢ (A \neq \emptyset \land \forall x \in A B = C) \to ⋂_{x \in A} B \subseteq C$
6		eqimss2	$⊢ B = C \to C \subseteq B$
7	6	ralimi	$⊢ \forall x \in A B = C \to \forall x \in A C \subseteq B$
8	7	adantl	$⊢ (A \neq \emptyset \land \forall x \in A B = C) \to \forall x \in A C \subseteq B$
9		ssiin	$⊢ C \subseteq ⋂_{x \in A} B \leftrightarrow \forall x \in A C \subseteq B$
10	8 9	sylibr	$⊢ (A \neq \emptyset \land \forall x \in A B = C) \to C \subseteq ⋂_{x \in A} B$
11	5 10	eqssd	$⊢ (A \neq \emptyset \land \forall x \in A B = C) \to ⋂_{x \in A} B = C$

Metamath Proof Explorer