Theorem mosssn

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

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

Proof

Step	Hyp	Ref	Expression
1		sssn	$$⊢A\subseteq \left\{B\right\}\leftrightarrow \left(A=\varnothing \vee A=\left\{B\right\}\right)$$
2		mo0	$$⊢A=\varnothing \to {\exists }^{*}xx\in A$$
3		mosn	$$⊢A=\left\{B\right\}\to {\exists }^{*}xx\in A$$
4	2 3	jaoi	$$⊢\left(A=\varnothing \vee A=\left\{B\right\}\right)\to {\exists }^{*}xx\in A$$
5	1 4	sylbi	$$⊢A\subseteq \left\{B\right\}\to {\exists }^{*}xx\in A$$