Theorem modom

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

	Ref	Expression
Assertion	modom	$$⊢{\exists }^{*}x\phi \leftrightarrow \left\{x|\phi \right\}\preccurlyeq 1_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		moeu	$$⊢{\exists }^{*}x\phi \leftrightarrow \left(\exists x\phi \to \exists !x\phi \right)$$
2		imor	$$⊢\left(\exists x\phi \to \exists !x\phi \right)\leftrightarrow \left(\neg \exists x\phi \vee \exists !x\phi \right)$$
3		abn0	$$⊢\left\{x|\phi \right\}\ne \varnothing \leftrightarrow \exists x\phi$$
4	3	necon1bbii	$$⊢\neg \exists x\phi \leftrightarrow \left\{x|\phi \right\}=\varnothing$$
5		sdom1	$$⊢\left\{x|\phi \right\}\prec 1_{𝑜}\leftrightarrow \left\{x|\phi \right\}=\varnothing$$
6	4 5	bitr4i	$$⊢\neg \exists x\phi \leftrightarrow \left\{x|\phi \right\}\prec 1_{𝑜}$$
7		euen1	$$⊢\exists !x\phi \leftrightarrow \left\{x|\phi \right\}\approx 1_{𝑜}$$
8	6 7	orbi12i	$$⊢\left(\neg \exists x\phi \vee \exists !x\phi \right)\leftrightarrow \left(\left\{x|\phi \right\}\prec 1_{𝑜}\vee \left\{x|\phi \right\}\approx 1_{𝑜}\right)$$
9		brdom2	$$⊢\left\{x|\phi \right\}\preccurlyeq 1_{𝑜}\leftrightarrow \left(\left\{x|\phi \right\}\prec 1_{𝑜}\vee \left\{x|\phi \right\}\approx 1_{𝑜}\right)$$
10	8 9	bitr4i	$$⊢\left(\neg \exists x\phi \vee \exists !x\phi \right)\leftrightarrow \left\{x|\phi \right\}\preccurlyeq 1_{𝑜}$$
11	1 2 10	3bitri	$$⊢{\exists }^{*}x\phi \leftrightarrow \left\{x|\phi \right\}\preccurlyeq 1_{𝑜}$$