Metamath Proof Explorer

Theorem ssunieq

Description: Relationship implying union. (Contributed by NM, 10-Nov-1999)

Ref Expression
Assertion ssunieq 
|- ( ( A e. B /\ A. x e. B x C_ A ) -> A = U. B )

Proof

Step Hyp Ref Expression
1 elssuni 
 |-  ( A e. B -> A C_ U. B )
2 unissb 
 |-  ( U. B C_ A <-> A. x e. B x C_ A )
3 2 biimpri 
 |-  ( A. x e. B x C_ A -> U. B C_ A )
4 1 3 anim12i 
 |-  ( ( A e. B /\ A. x e. B x C_ A ) -> ( A C_ U. B /\ U. B C_ A ) )
5 eqss 
 |-  ( A = U. B <-> ( A C_ U. B /\ U. B C_ A ) )
6 4 5 sylibr 
 |-  ( ( A e. B /\ A. x e. B x C_ A ) -> A = U. B )