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	|- { x | E. y x = { y } } e/ _V

Proof

Step	Hyp	Ref	Expression
1		abnex	|- ( A. y ( { y } e. _V /\ y e. { y } ) -> -. { x | E. y x = { y } } e. _V )
2		df-nel	|- ( { x | E. y x = { y } } e/ _V <-> -. { x | E. y x = { y } } e. _V )
3	1 2	sylibr	|- ( A. y ( { y } e. _V /\ y e. { y } ) -> { x | E. y x = { y } } e/ _V )
4		snex	|- { y } e. _V
5		vsnid	|- y e. { y }
6	4 5	pm3.2i	|- ( { y } e. _V /\ y e. { y } )
7	3 6	mpg	|- { x | E. y x = { y } } e/ _V