Theorem mosn

Description: "At most one" element in a singleton. (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Assertion	mosn	$$⊢A=\left\{B\right\}\to {\exists }^{*}xx\in A$$

Proof

Step	Hyp	Ref	Expression
1		rmosn	$$⊢{\exists }^{*}x\in \left\{B\right\}\top$$
2		rmotru	$$⊢{\exists }^{*}xx\in \left\{B\right\}\leftrightarrow {\exists }^{*}x\in \left\{B\right\}\top$$
3	1 2	mpbir	$$⊢{\exists }^{*}xx\in \left\{B\right\}$$
4		eleq2	$$⊢A=\left\{B\right\}\to \left(x\in A\leftrightarrow x\in \left\{B\right\}\right)$$
5	4	mobidv	$$⊢A=\left\{B\right\}\to \left({\exists }^{*}xx\in A\leftrightarrow {\exists }^{*}xx\in \left\{B\right\}\right)$$
6	3 5	mpbiri	$$⊢A=\left\{B\right\}\to {\exists }^{*}xx\in A$$