Metamath Proof Explorer

Theorem iuneqconst2

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

Ref Expression
Assertion iuneqconst2 
|- ( ( A =/= (/) /\ A. x e. A B = C ) -> U_ x e. A B = C )

Proof

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