Metamath Proof Explorer


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