Metamath Proof Explorer

Theorem unss1

Description: Subclass law for union of classes. (Contributed by NM, 14-Oct-1999) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion unss1 ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ 𝐶 ) ⊆ ( 𝐵 ∪ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
2 1 orim1d ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶 ) ) )
3 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶 ) )
4 elun ⊢ ( 𝑥 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶 ) )
5 2 3 4 3imtr4g ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ ( 𝐴 ∪ 𝐶 ) → 𝑥 ∈ ( 𝐵 ∪ 𝐶 ) ) )
6 5 ssrdv ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ 𝐶 ) ⊆ ( 𝐵 ∪ 𝐶 ) )