Theorem reuen1

Description: Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014)

	Ref	Expression
Assertion	reuen1	$$⊢\exists !x\in A\phi \leftrightarrow \left\{x\in A|\phi \right\}\approx 1_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		reusn	$$⊢\exists !x\in A\phi \leftrightarrow \exists y\left\{x\in A|\phi \right\}=\left\{y\right\}$$
2		en1	$$⊢\left\{x\in A|\phi \right\}\approx 1_{𝑜}\leftrightarrow \exists y\left\{x\in A|\phi \right\}=\left\{y\right\}$$
3	1 2	bitr4i	$$⊢\exists !x\in A\phi \leftrightarrow \left\{x\in A|\phi \right\}\approx 1_{𝑜}$$