Theorem pssn0

Description: A proper superset is nonempty. (Contributed by Steven Nguyen, 17-Jul-2022)

	Ref	Expression
Assertion	pssn0	⊢ ( 𝐴 ⊊ 𝐵 → 𝐵 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		npss0	⊢ ¬ 𝐴 ⊊ ∅
2		psseq2	⊢ ( 𝐵 = ∅ → ( 𝐴 ⊊ 𝐵 ↔ 𝐴 ⊊ ∅ ) )
3	1 2	mtbiri	⊢ ( 𝐵 = ∅ → ¬ 𝐴 ⊊ 𝐵 )
4	3	necon2ai	⊢ ( 𝐴 ⊊ 𝐵 → 𝐵 ≠ ∅ )