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

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