Theorem vss

Description: Only the universal class has the universal class as a subclass. (Contributed by NM, 17-Sep-2003) (Proof shortened by Andrew Salmon, 26-Jun-2011)

	Ref	Expression
Assertion	vss	$$⊢\mathrm{V}\subseteq A\leftrightarrow A=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ssv	$$⊢A\subseteq \mathrm{V}$$
2	1	biantrur	$$⊢\mathrm{V}\subseteq A\leftrightarrow \left(A\subseteq \mathrm{V}\wedge \mathrm{V}\subseteq A\right)$$
3		eqss	$$⊢A=\mathrm{V}\leftrightarrow \left(A\subseteq \mathrm{V}\wedge \mathrm{V}\subseteq A\right)$$
4	2 3	bitr4i	$$⊢\mathrm{V}\subseteq A\leftrightarrow A=\mathrm{V}$$