Metamath Proof Explorer


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 ( 𝐴𝑉 → ¬ { 𝐴 } ∈ 𝐴 )