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	$$⊢\left(C\in B\wedge B\ne \left\{A\right\}\right)\to \exists x\in Bx\ne A$$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$$⊢C\in B\to B\ne \varnothing$$
2		eqsn	$$⊢B\ne \varnothing \to \left(B=\left\{A\right\}\leftrightarrow \forall x\in Bx=A\right)$$
3	1 2	syl	$$⊢C\in B\to \left(B=\left\{A\right\}\leftrightarrow \forall x\in Bx=A\right)$$
4	3	biimprd	$$⊢C\in B\to \left(\forall x\in Bx=A\to B=\left\{A\right\}\right)$$
5	4	con3d	$$⊢C\in B\to \left(\neg B=\left\{A\right\}\to \neg \forall x\in Bx=A\right)$$
6		df-ne	$$⊢B\ne \left\{A\right\}\leftrightarrow \neg B=\left\{A\right\}$$
7		nne	$$⊢\neg x\ne A\leftrightarrow x=A$$
8	7	bicomi	$$⊢x=A\leftrightarrow \neg x\ne A$$
9	8	ralbii	$$⊢\forall x\in Bx=A\leftrightarrow \forall x\in B\neg x\ne A$$
10		ralnex	$$⊢\forall x\in B\neg x\ne A\leftrightarrow \neg \exists x\in Bx\ne A$$
11	9 10	bitri	$$⊢\forall x\in Bx=A\leftrightarrow \neg \exists x\in Bx\ne A$$
12	11	con2bii	$$⊢\exists x\in Bx\ne A\leftrightarrow \neg \forall x\in Bx=A$$
13	5 6 12	3imtr4g	$$⊢C\in B\to \left(B\ne \left\{A\right\}\to \exists x\in Bx\ne A\right)$$
14	13	imp	$$⊢\left(C\in B\wedge B\ne \left\{A\right\}\right)\to \exists x\in Bx\ne A$$