Theorem bj-nsnid

Description: A set does not contain the singleton formed on it. More precisely, one can prove that a class contains the singleton formed on it if and only if it is proper and contains the empty set (since it is "the singleton formed on" any proper class, see snprc ): |- -. ( { A } e. A <-> ( (/) e. A -> A e. _V ) ) . (Contributed by BJ, 4-Feb-2023)

	Ref	Expression
Assertion	bj-nsnid	⊢ ( 𝐴 ∈ 𝑉 → ¬ { 𝐴 } ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		en2lp	⊢ ¬ ( 𝐴 ∈ { 𝐴 } ∧ { 𝐴 } ∈ 𝐴 )
2		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
3	2	anim1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝐴 } ∈ 𝐴 ) → ( 𝐴 ∈ { 𝐴 } ∧ { 𝐴 } ∈ 𝐴 ) )
4	3	ex	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } ∈ 𝐴 → ( 𝐴 ∈ { 𝐴 } ∧ { 𝐴 } ∈ 𝐴 ) ) )
5	1 4	mtoi	⊢ ( 𝐴 ∈ 𝑉 → ¬ { 𝐴 } ∈ 𝐴 )