Metamath Proof Explorer


Theorem unss2

Description: Subclass law for union of classes. Exercise 7 of TakeutiZaring p. 18. (Contributed by NM, 14-Oct-1999)

Ref Expression
Assertion unss2 A B C A C B

Proof

Step Hyp Ref Expression
1 unss1 A B A C B C
2 uncom C A = A C
3 uncom C B = B C
4 1 2 3 3sstr4g A B C A C B