Metamath Proof Explorer


Theorem ssequn2

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

Ref Expression
Assertion ssequn2 ABBA=B

Proof

Step Hyp Ref Expression
1 ssequn1 ABAB=B
2 uncom AB=BA
3 2 eqeq1i AB=BBA=B
4 1 3 bitri ABBA=B