Metamath Proof Explorer


Theorem ssun

Description: A condition that implies inclusion in the union of two classes. (Contributed by NM, 23-Nov-2003)

Ref Expression
Assertion ssun ( ( 𝐴𝐵𝐴𝐶 ) → 𝐴 ⊆ ( 𝐵𝐶 ) )

Proof

Step Hyp Ref Expression
1 ssun3 ( 𝐴𝐵𝐴 ⊆ ( 𝐵𝐶 ) )
2 ssun4 ( 𝐴𝐶𝐴 ⊆ ( 𝐵𝐶 ) )
3 1 2 jaoi ( ( 𝐴𝐵𝐴𝐶 ) → 𝐴 ⊆ ( 𝐵𝐶 ) )