Theorem vsn

Description: The singleton of the universal class is the empty set. (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Assertion	vsn	$$⊢\left\{\mathrm{V}\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		vprc	$$⊢\neg \mathrm{V}\in \mathrm{V}$$
2		snprc	$$⊢\neg \mathrm{V}\in \mathrm{V}\leftrightarrow \left\{\mathrm{V}\right\}=\varnothing$$
3	1 2	mpbi	$$⊢\left\{\mathrm{V}\right\}=\varnothing$$