Theorem intssuni2

Description: Subclass relationship for intersection and union. (Contributed by NM, 29-Jul-2006)

	Ref	Expression
Assertion	intssuni2	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ⊆ ∪ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		intssuni	⊢ ( 𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴 )
2		uniss	⊢ ( 𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵 )
3	1 2	sylan9ssr	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ⊆ ∪ 𝐵 )