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	⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝐵 ≠ { 𝐴 } ) → ∃ 𝑥 ∈ 𝐵 𝑥 ≠ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ne0i	⊢ ( 𝐶 ∈ 𝐵 → 𝐵 ≠ ∅ )
2		eqsn	⊢ ( 𝐵 ≠ ∅ → ( 𝐵 = { 𝐴 } ↔ ∀ 𝑥 ∈ 𝐵 𝑥 = 𝐴 ) )
3	1 2	syl	⊢ ( 𝐶 ∈ 𝐵 → ( 𝐵 = { 𝐴 } ↔ ∀ 𝑥 ∈ 𝐵 𝑥 = 𝐴 ) )
4	3	biimprd	⊢ ( 𝐶 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝑥 = 𝐴 → 𝐵 = { 𝐴 } ) )
5	4	con3d	⊢ ( 𝐶 ∈ 𝐵 → ( ¬ 𝐵 = { 𝐴 } → ¬ ∀ 𝑥 ∈ 𝐵 𝑥 = 𝐴 ) )
6		df-ne	⊢ ( 𝐵 ≠ { 𝐴 } ↔ ¬ 𝐵 = { 𝐴 } )
7		nne	⊢ ( ¬ 𝑥 ≠ 𝐴 ↔ 𝑥 = 𝐴 )
8	7	bicomi	⊢ ( 𝑥 = 𝐴 ↔ ¬ 𝑥 ≠ 𝐴 )
9	8	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ≠ 𝐴 )
10		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ≠ 𝐴 ↔ ¬ ∃ 𝑥 ∈ 𝐵 𝑥 ≠ 𝐴 )
11	9 10	bitri	⊢ ( ∀ 𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ¬ ∃ 𝑥 ∈ 𝐵 𝑥 ≠ 𝐴 )
12	11	con2bii	⊢ ( ∃ 𝑥 ∈ 𝐵 𝑥 ≠ 𝐴 ↔ ¬ ∀ 𝑥 ∈ 𝐵 𝑥 = 𝐴 )
13	5 6 12	3imtr4g	⊢ ( 𝐶 ∈ 𝐵 → ( 𝐵 ≠ { 𝐴 } → ∃ 𝑥 ∈ 𝐵 𝑥 ≠ 𝐴 ) )
14	13	imp	⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝐵 ≠ { 𝐴 } ) → ∃ 𝑥 ∈ 𝐵 𝑥 ≠ 𝐴 )