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 
|- ( ( 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 )