Definition df-bj-mo

Description: Definition of the uniqueness quantifier which is correct on the empty domain. Instead of the fresh variable z , one could save a dummy variable by using x or y at the cost of having nested quantifiers on the same variable. (Contributed by BJ, 12-Mar-2023)

	Ref	Expression
Assertion	df-bj-mo	$$⊢{\exists }^{**}x\phi \leftrightarrow \forall z\exists y\forall x\left(\phi \to x=y\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		wph	$$wff\phi$$
2	1 0	wmoo	$$wff{\exists }^{**}x\phi$$
3		vz	$$setvarz$$
4		vy	$$setvary$$
5	0	cv	$$setvarx$$
6	4	cv	$$setvary$$
7	5 6	wceq	$$wffx=y$$
8	1 7	wi	$$wff\left(\phi \to x=y\right)$$
9	8 0	wal	$$wff\forall x\left(\phi \to x=y\right)$$
10	9 4	wex	$$wff\exists y\forall x\left(\phi \to x=y\right)$$
11	10 3	wal	$$wff\forall z\exists y\forall x\left(\phi \to x=y\right)$$
12	2 11	wb	$$wff\left({\exists }^{**}x\phi \leftrightarrow \forall z\exists y\forall x\left(\phi \to x=y\right)\right)$$