This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem n0nsnel

Description: If a class with one element is not a singleton, there is at least another element in this class. (Contributed by AV, 6-Mar-2025) (Revised by Thierry Arnoux, 28-May-2025)

Ref Expression
Assertion n0nsnel 
|- ( ( C e. B /\ B =/= { A } ) -> E. x e. B x =/= A )

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( C e. B -> B =/= (/) )
2 eqsn 
 |-  ( B =/= (/) -> ( B = { A } <-> A. x e. B x = A ) )
3 1 2 syl 
 |-  ( C e. B -> ( B = { A } <-> A. x e. B x = A ) )
4 3 biimprd 
 |-  ( C e. B -> ( A. x e. B x = A -> B = { A } ) )
5 4 con3d 
 |-  ( C e. B -> ( -. B = { A } -> -. A. x e. B x = A ) )
6 df-ne 
 |-  ( B =/= { A } <-> -. B = { A } )
7 nne 
 |-  ( -. x =/= A <-> x = A )
8 7 bicomi 
 |-  ( x = A <-> -. x =/= A )
9 8 ralbii 
 |-  ( A. x e. B x = A <-> A. x e. B -. x =/= A )
10 ralnex 
 |-  ( A. x e. B -. x =/= A <-> -. E. x e. B x =/= A )
11 9 10 bitri 
 |-  ( A. x e. B x = A <-> -. E. x e. B x =/= A )
12 11 con2bii 
 |-  ( E. x e. B x =/= A <-> -. A. x e. B x = A )
13 5 6 12 3imtr4g 
 |-  ( C e. B -> ( B =/= { A } -> E. x e. B x =/= A ) )
14 13 imp 
 |-  ( ( C e. B /\ B =/= { A } ) -> E. x e. B x =/= A )