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	syl6bi	⊢ ( 𝐵 = { 𝑥 } → ( 𝐴 ∈ 𝐵 → { 𝐴 } = { 𝑥 } ) )
6	5	imp	⊢ ( ( 𝐵 = { 𝑥 } ∧ 𝐴 ∈ 𝐵 ) → { 𝐴 } = { 𝑥 } )
7		eqtr3	⊢ ( ( 𝐵 = { 𝑥 } ∧ { 𝐴 } = { 𝑥 } ) → 𝐵 = { 𝐴 } )
8	6 7	syldan	⊢ ( ( 𝐵 = { 𝑥 } ∧ 𝐴 ∈ 𝐵 ) → 𝐵 = { 𝐴 } )
9	8	ex	⊢ ( 𝐵 = { 𝑥 } → ( 𝐴 ∈ 𝐵 → 𝐵 = { 𝐴 } ) )
10	9	exlimiv	⊢ ( ∃ 𝑥 𝐵 = { 𝑥 } → ( 𝐴 ∈ 𝐵 → 𝐵 = { 𝐴 } ) )
11	1 10	sylbi	⊢ ( 𝐵 ≈ 1o → ( 𝐴 ∈ 𝐵 → 𝐵 = { 𝐴 } ) )
12	11	impcom	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o ) → 𝐵 = { 𝐴 } )