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 ( 𝐴𝐵 → ( 𝐶𝐴 ) ⊆ ( 𝐶𝐵 ) )

Proof

Step Hyp Ref Expression
1 unss1 ( 𝐴𝐵 → ( 𝐴𝐶 ) ⊆ ( 𝐵𝐶 ) )
2 uncom ( 𝐶𝐴 ) = ( 𝐴𝐶 )
3 uncom ( 𝐶𝐵 ) = ( 𝐵𝐶 )
4 1 2 3 3sstr4g ( 𝐴𝐵 → ( 𝐶𝐴 ) ⊆ ( 𝐶𝐵 ) )