Metamath Proof Explorer


Theorem ssun2

Description: Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993)

Ref Expression
Assertion ssun2 ⊢ A ⊆ B ∪ A

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ A ⊆ A ∪ B
2 uncom ⊢ A ∪ B = B ∪ A
3 1 2 sseqtri ⊢ A ⊆ B ∪ A