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 )