Theorem en1eqsn

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

	Ref	Expression
Assertion	en1eqsn	$$⊢\left(A\in B\wedge B\approx 1_{𝑜}\right)\to B=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
2		ssid	$$⊢1_{𝑜}\subseteq 1_{𝑜}$$
3		ssnnfi	$$⊢\left(1_{𝑜}\in \mathrm{\omega }\wedge 1_{𝑜}\subseteq 1_{𝑜}\right)\to 1_{𝑜}\in \mathrm{Fin}$$
4	1 2 3	mp2an	$$⊢1_{𝑜}\in \mathrm{Fin}$$
5		enfii	$$⊢\left(1_{𝑜}\in \mathrm{Fin}\wedge B\approx 1_{𝑜}\right)\to B\in \mathrm{Fin}$$
6	4 5	mpan	$$⊢B\approx 1_{𝑜}\to B\in \mathrm{Fin}$$
7	6	adantl	$$⊢\left(A\in B\wedge B\approx 1_{𝑜}\right)\to B\in \mathrm{Fin}$$
8		snssi	$$⊢A\in B\to \left\{A\right\}\subseteq B$$
9	8	adantr	$$⊢\left(A\in B\wedge B\approx 1_{𝑜}\right)\to \left\{A\right\}\subseteq B$$
10		ensn1g	$$⊢A\in B\to \left\{A\right\}\approx 1_{𝑜}$$
11		ensym	$$⊢B\approx 1_{𝑜}\to 1_{𝑜}\approx B$$
12		entr	$$⊢\left(\left\{A\right\}\approx 1_{𝑜}\wedge 1_{𝑜}\approx B\right)\to \left\{A\right\}\approx B$$
13	10 11 12	syl2an	$$⊢\left(A\in B\wedge B\approx 1_{𝑜}\right)\to \left\{A\right\}\approx B$$
14		fisseneq	$$⊢\left(B\in \mathrm{Fin}\wedge \left\{A\right\}\subseteq B\wedge \left\{A\right\}\approx B\right)\to \left\{A\right\}=B$$
15	7 9 13 14	syl3anc	$$⊢\left(A\in B\wedge B\approx 1_{𝑜}\right)\to \left\{A\right\}=B$$
16	15	eqcomd	$$⊢\left(A\in B\wedge B\approx 1_{𝑜}\right)\to B=\left\{A\right\}$$