Theorem ssn0

Description: A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007)

	Ref	Expression
Assertion	ssn0	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) → 𝐵 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		sseq0	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅ ) → 𝐴 = ∅ )
2	1	ex	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 = ∅ → 𝐴 = ∅ ) )
3	2	necon3d	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ≠ ∅ → 𝐵 ≠ ∅ ) )
4	3	imp	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) → 𝐵 ≠ ∅ )