Theorem nvpss

Description: No class strictly includes the universal class. Dual of npss0 . (Contributed by BJ, 12-Jul-2026)

	Ref	Expression
Assertion	nvpss	$$⊢\neg \mathrm{V}\subset A$$

Proof

Step	Hyp	Ref	Expression
1		ssv	$$⊢A\subseteq \mathrm{V}$$
2		ssnpss	$$⊢A\subseteq \mathrm{V}\to \neg \mathrm{V}\subset A$$
3	1 2	ax-mp	$$⊢\neg \mathrm{V}\subset A$$