Theorem mosssn2

Description: Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 23-Sep-2024)

	Ref	Expression
Assertion	mosssn2	$$⊢{\exists }^{*}xx\in A\leftrightarrow \exists yA\subseteq \left\{y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		19.45v	$$⊢\exists y\left(A=\varnothing \vee A=\left\{y\right\}\right)\leftrightarrow \left(A=\varnothing \vee \exists yA=\left\{y\right\}\right)$$
2		sssn	$$⊢A\subseteq \left\{y\right\}\leftrightarrow \left(A=\varnothing \vee A=\left\{y\right\}\right)$$
3	2	exbii	$$⊢\exists yA\subseteq \left\{y\right\}\leftrightarrow \exists y\left(A=\varnothing \vee A=\left\{y\right\}\right)$$
4		mo0sn	$$⊢{\exists }^{*}xx\in A\leftrightarrow \left(A=\varnothing \vee \exists yA=\left\{y\right\}\right)$$
5	1 3 4	3bitr4ri	$$⊢{\exists }^{*}xx\in A\leftrightarrow \exists yA\subseteq \left\{y\right\}$$