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	$⊢ \{x \| \exists y x = \{y\}\} \notin V$

Proof

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

Metamath Proof Explorer

Theorem snnex

Proof