Theorem en1eqsn

Description: A set with one element is a singleton. (Contributed by FL, 18-Aug-2008)

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

Proof

Step	Hyp	Ref	Expression
1		1onn	⊢ 1o ∈ ω
2		ssid	⊢ 1o ⊆ 1o
3		ssnnfi	⊢ ( ( 1o ∈ ω ∧ 1o ⊆ 1o ) → 1o ∈ Fin )
4	1 2 3	mp2an	⊢ 1o ∈ Fin
5		enfii	⊢ ( ( 1o ∈ Fin ∧ 𝐵 ≈ 1o ) → 𝐵 ∈ Fin )
6	4 5	mpan	⊢ ( 𝐵 ≈ 1o → 𝐵 ∈ Fin )
7	6	adantl	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o ) → 𝐵 ∈ Fin )
8		snssi	⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ⊆ 𝐵 )
9	8	adantr	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o ) → { 𝐴 } ⊆ 𝐵 )
10		ensn1g	⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ≈ 1o )
11		ensym	⊢ ( 𝐵 ≈ 1o → 1o ≈ 𝐵 )
12		entr	⊢ ( ( { 𝐴 } ≈ 1o ∧ 1o ≈ 𝐵 ) → { 𝐴 } ≈ 𝐵 )
13	10 11 12	syl2an	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o ) → { 𝐴 } ≈ 𝐵 )
14		fisseneq	⊢ ( ( 𝐵 ∈ Fin ∧ { 𝐴 } ⊆ 𝐵 ∧ { 𝐴 } ≈ 𝐵 ) → { 𝐴 } = 𝐵 )
15	7 9 13 14	syl3anc	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o ) → { 𝐴 } = 𝐵 )
16	15	eqcomd	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o ) → 𝐵 = { 𝐴 } )