This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mo0

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

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

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