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

Metamath Proof Explorer

Theorem reutru

Description: Two ways of expressing "exactly one" element. (Contributed by Zhi Wang, 23-Sep-2024)

		Ref	Expression
	Assertion	reutru	$⊢ \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	eubii	$⊢ \exists! x x \in A \leftrightarrow \exists! x (x \in A \land ⊤)$
4		df-reu	$⊢ \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 ⊤$