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

Metamath Proof Explorer

Theorem rmotru

Description: Two ways of expressing "at most one" element. (Contributed by Zhi Wang, 19-Sep-2024) (Proof shortened by BJ, 23-Sep-2024)

		Ref	Expression
	Assertion	rmotru	$⊢ \exists^{} x x \in A \leftrightarrow \exists^{} x \in A ⊤$

Step	Hyp	Ref	Expression
1		tru	$⊢ ⊤$
2	1	biantru	$⊢ x \in A \leftrightarrow (x \in A \land ⊤)$
3	2	mobii	$⊢ \exists^{} x x \in A \leftrightarrow \exists^{} x (x \in A \land ⊤)$
4		df-rmo	$⊢ \exists^{} x \in A ⊤ \leftrightarrow \exists^{} x (x \in A \land ⊤)$
5	3 4	bitr4i	$⊢ \exists^{} x x \in A \leftrightarrow \exists^{} x \in A ⊤$