Theorem pssv

Description: Any non-universal class is a proper subclass of the universal class. (Contributed by NM, 17-May-1998)

	Ref	Expression
Assertion	pssv	$$⊢A\subset \mathrm{V}\leftrightarrow \neg A=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ssv	$$⊢A\subseteq \mathrm{V}$$
2		dfpss2	$$⊢A\subset \mathrm{V}\leftrightarrow \left(A\subseteq \mathrm{V}\wedge \neg A=\mathrm{V}\right)$$
3	1 2	mpbiran	$$⊢A\subset \mathrm{V}\leftrightarrow \neg A=\mathrm{V}$$