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 |
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 |