Metamath Proof Explorer

Theorem unissel

Description: Condition turning a subclass relationship for union into an equality. (Contributed by NM, 18-Jul-2006)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( U. A C_ B /\ B e. A ) -> U. A C_ B )
2 elssuni 
 |-  ( B e. A -> B C_ U. A )
3 2 adantl 
 |-  ( ( U. A C_ B /\ B e. A ) -> B C_ U. A )
4 1 3 eqssd 
 |-  ( ( U. A C_ B /\ B e. A ) -> U. A = B )