Theorem euen1

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

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

Proof

Step	Hyp	Ref	Expression
1		reuen1	$$⊢\exists !x\in \mathrm{V}\phi \leftrightarrow \left\{x\in \mathrm{V}|\phi \right\}\approx 1_{𝑜}$$
2		reuv	$$⊢\exists !x\in \mathrm{V}\phi \leftrightarrow \exists !x\phi$$
3		rabab	$$⊢\left\{x\in \mathrm{V}|\phi \right\}=\left\{x|\phi \right\}$$
4	3	breq1i	$$⊢\left\{x\in \mathrm{V}|\phi \right\}\approx 1_{𝑜}\leftrightarrow \left\{x|\phi \right\}\approx 1_{𝑜}$$
5	1 2 4	3bitr3i	$$⊢\exists !x\phi \leftrightarrow \left\{x|\phi \right\}\approx 1_{𝑜}$$