Theorem iineqconst2

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

	Ref	Expression
Assertion	iineqconst2	|- ( ( A =/= (/) /\ A. x e. A B = C ) -> |^|_ x e. A B = C )

Proof

Step	Hyp	Ref	Expression
1		r19.2z	|- ( ( A =/= (/) /\ A. x e. A B = C ) -> E. x e. A B = C )
2		eqimss	|- ( B = C -> B C_ C )
3	2	reximi	|- ( E. x e. A B = C -> E. x e. A B C_ C )
4		iinss	|- ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )
5	1 3 4	3syl	|- ( ( A =/= (/) /\ A. x e. A B = C ) -> |^|_ x e. A B C_ C )
6		eqimss2	|- ( B = C -> C C_ B )
7	6	ralimi	|- ( A. x e. A B = C -> A. x e. A C C_ B )
8	7	adantl	|- ( ( A =/= (/) /\ A. x e. A B = C ) -> A. x e. A C C_ B )
9		ssiin	|- ( C C_ |^|_ x e. A B <-> A. x e. A C C_ B )
10	8 9	sylibr	|- ( ( A =/= (/) /\ A. x e. A B = C ) -> C C_ |^|_ x e. A B )
11	5 10	eqssd	|- ( ( A =/= (/) /\ A. x e. A B = C ) -> |^|_ x e. A B = C )