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	⊢ { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ∉ V

Proof

Step	Hyp	Ref	Expression
1		abnex	⊢ ( ∀ 𝑦 ( { 𝑦 } ∈ V ∧ 𝑦 ∈ { 𝑦 } ) → ¬ { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ∈ V )
2		df-nel	⊢ ( { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ∉ V ↔ ¬ { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ∈ V )
3	1 2	sylibr	⊢ ( ∀ 𝑦 ( { 𝑦 } ∈ V ∧ 𝑦 ∈ { 𝑦 } ) → { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ∉ V )
4		snex	⊢ { 𝑦 } ∈ V
5		vsnid	⊢ 𝑦 ∈ { 𝑦 }
6	4 5	pm3.2i	⊢ ( { 𝑦 } ∈ V ∧ 𝑦 ∈ { 𝑦 } )
7	3 6	mpg	⊢ { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ∉ V