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

Metamath Proof Explorer

Theorem euhash1

Description: The size of a set is 1 in terms of existential uniqueness. (Contributed by Alexander van der Vekens, 8-Feb-2018)

		Ref	Expression
	Assertion	euhash1	$⊢ V \in W \to (\|V\| = 1 \leftrightarrow \exists! a a \in V)$

Step	Hyp	Ref	Expression
1		hashen1	$⊢ V \in W \to (\|V\| = 1 \leftrightarrow V \approx 1_{𝑜})$
2		euen1b	$⊢ V \approx 1_{𝑜} \leftrightarrow \exists! a a \in V$
3	1 2	bitrdi	$⊢ V \in W \to (\|V\| = 1 \leftrightarrow \exists! a a \in V)$