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	$$⊢\left(A\in B\wedge B\approx 1_{𝑜}\right)\to B=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		en1	$$⊢B\approx 1_{𝑜}\leftrightarrow \exists xB=\left\{x\right\}$$
2		eleq2	$$⊢B=\left\{x\right\}\to \left(A\in B\leftrightarrow A\in \left\{x\right\}\right)$$
3		elsni	$$⊢A\in \left\{x\right\}\to A=x$$
4	3	sneqd	$$⊢A\in \left\{x\right\}\to \left\{A\right\}=\left\{x\right\}$$
5	2 4	biimtrdi	$$⊢B=\left\{x\right\}\to \left(A\in B\to \left\{A\right\}=\left\{x\right\}\right)$$
6	5	imp	$$⊢\left(B=\left\{x\right\}\wedge A\in B\right)\to \left\{A\right\}=\left\{x\right\}$$
7		eqtr3	$$⊢\left(B=\left\{x\right\}\wedge \left\{A\right\}=\left\{x\right\}\right)\to B=\left\{A\right\}$$
8	6 7	syldan	$$⊢\left(B=\left\{x\right\}\wedge A\in B\right)\to B=\left\{A\right\}$$
9	8	ex	$$⊢B=\left\{x\right\}\to \left(A\in B\to B=\left\{A\right\}\right)$$
10	9	exlimiv	$$⊢\exists xB=\left\{x\right\}\to \left(A\in B\to B=\left\{A\right\}\right)$$
11	1 10	sylbi	$$⊢B\approx 1_{𝑜}\to \left(A\in B\to B=\left\{A\right\}\right)$$
12	11	impcom	$$⊢\left(A\in B\wedge B\approx 1_{𝑜}\right)\to B=\left\{A\right\}$$