Theorem snnex

Description: The class of all singletons is a proper class. See also pwnex . (Contributed by NM, 10-Oct-2008) (Proof shortened by Eric Schmidt, 7-Dec-2008) (Proof shortened by BJ, 5-Dec-2021)

	Ref	Expression
Assertion	snnex	$$⊢\left\{x|\exists yx=\left\{y\right\}\right\}\notin \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		abnex	$$⊢\forall y\left(\left\{y\right\}\in \mathrm{V}\wedge y\in \left\{y\right\}\right)\to \neg \left\{x|\exists yx=\left\{y\right\}\right\}\in \mathrm{V}$$
2		df-nel	$$⊢\left\{x|\exists yx=\left\{y\right\}\right\}\notin \mathrm{V}\leftrightarrow \neg \left\{x|\exists yx=\left\{y\right\}\right\}\in \mathrm{V}$$
3	1 2	sylibr	$$⊢\forall y\left(\left\{y\right\}\in \mathrm{V}\wedge y\in \left\{y\right\}\right)\to \left\{x|\exists yx=\left\{y\right\}\right\}\notin \mathrm{V}$$
4		snex	$$⊢\left\{y\right\}\in \mathrm{V}$$
5		vsnid	$$⊢y\in \left\{y\right\}$$
6	4 5	pm3.2i	$$⊢\left(\left\{y\right\}\in \mathrm{V}\wedge y\in \left\{y\right\}\right)$$
7	3 6	mpg	$$⊢\left\{x|\exists yx=\left\{y\right\}\right\}\notin \mathrm{V}$$