Theorem mo0

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

	Ref	Expression
Assertion	mo0	$$⊢A=\varnothing \to {\exists }^{*}xx\in A$$

Proof

Step	Hyp	Ref	Expression
1		vsn	$$⊢\left\{\mathrm{V}\right\}=\varnothing$$
2	1	eqcomi	$$⊢\varnothing =\left\{\mathrm{V}\right\}$$
3		eqeq1	$$⊢A=\varnothing \to \left(A=\left\{\mathrm{V}\right\}\leftrightarrow \varnothing =\left\{\mathrm{V}\right\}\right)$$
4	2 3	mpbiri	$$⊢A=\varnothing \to A=\left\{\mathrm{V}\right\}$$
5		mosn	$$⊢A=\left\{\mathrm{V}\right\}\to {\exists }^{*}xx\in A$$
6	4 5	syl	$$⊢A=\varnothing \to {\exists }^{*}xx\in A$$