This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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