Metamath Proof Explorer

Theorem ssequn2

Description: A relationship between subclass and union. (Contributed by NM, 13-Jun-1994)

Ref Expression
Assertion ssequn2 
|- ( A C_ B <-> ( B u. A ) = B )

Proof

Step Hyp Ref Expression
1 ssequn1 
 |-  ( A C_ B <-> ( A u. B ) = B )
2 uncom 
 |-  ( A u. B ) = ( B u. A )
3 2 eqeq1i 
 |-  ( ( A u. B ) = B <-> ( B u. A ) = B )
4 1 3 bitri 
 |-  ( A C_ B <-> ( B u. A ) = B )