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

Metamath Proof Explorer

Theorem euen1b

Description: Two ways to express " A has a unique element". (Contributed by Mario Carneiro, 9-Apr-2015)

		Ref	Expression
	Assertion	euen1b	$⊢ A \approx 1_{𝑜} \leftrightarrow \exists! x x \in A$

Step	Hyp	Ref	Expression
1		euen1	$⊢ \exists! x x \in A \leftrightarrow \{x \| x \in A\} \approx 1_{𝑜}$
2		abid2	$⊢ \{x \| x \in A\} = A$
3	2	breq1i	$⊢ \{x \| x \in A\} \approx 1_{𝑜} \leftrightarrow A \approx 1_{𝑜}$
4	1 3	bitr2i	$⊢ A \approx 1_{𝑜} \leftrightarrow \exists! x x \in A$