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 \left(\left|V\right|=1\leftrightarrow \exists !aa\in V\right)$$

Proof

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