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

Metamath Proof Explorer

Theorem en1eqsn

Description: A set with one element is a singleton. (Contributed by FL, 18-Aug-2008) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 4-Jan-2025)

Ref Expression
Assertion en1eqsn ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o ) → 𝐵 = { 𝐴 } )

Proof

Step Hyp Ref Expression
1 en1 ⊢ ( 𝐵 ≈ 1o ↔ ∃ 𝑥 𝐵 = { 𝑥 } )
2 eleq2 ⊢ ( 𝐵 = { 𝑥 } → ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ { 𝑥 } ) )
3 elsni ⊢ ( 𝐴 ∈ { 𝑥 } → 𝐴 = 𝑥 )
4 3 sneqd ⊢ ( 𝐴 ∈ { 𝑥 } → { 𝐴 } = { 𝑥 } )
5 2 4 biimtrdi ⊢ ( 𝐵 = { 𝑥 } → ( 𝐴 ∈ 𝐵 → { 𝐴 } = { 𝑥 } ) )
6 5 imp ⊢ ( ( 𝐵 = { 𝑥 } ∧ 𝐴 ∈ 𝐵 ) → { 𝐴 } = { 𝑥 } )
7 eqtr3 ⊢ ( ( 𝐵 = { 𝑥 } ∧ { 𝐴 } = { 𝑥 } ) → 𝐵 = { 𝐴 } )
8 6 7 syldan ⊢ ( ( 𝐵 = { 𝑥 } ∧ 𝐴 ∈ 𝐵 ) → 𝐵 = { 𝐴 } )
9 8 ex ⊢ ( 𝐵 = { 𝑥 } → ( 𝐴 ∈ 𝐵 → 𝐵 = { 𝐴 } ) )
10 9 exlimiv ⊢ ( ∃ 𝑥 𝐵 = { 𝑥 } → ( 𝐴 ∈ 𝐵 → 𝐵 = { 𝐴 } ) )
11 1 10 sylbi ⊢ ( 𝐵 ≈ 1o → ( 𝐴 ∈ 𝐵 → 𝐵 = { 𝐴 } ) )
12 11 impcom ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o ) → 𝐵 = { 𝐴 } )