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	|- ( E** x ph <-> A. z E. y A. x ( ph -> x = y ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		wph	|- ph
2	1 0	wmoo	|- E** x ph
3		vz	|- z
4		vy	|- y
5	0	cv	|- x
6	4	cv	|- y
7	5 6	wceq	|- x = y
8	1 7	wi	|- ( ph -> x = y )
9	8 0	wal	|- A. x ( ph -> x = y )
10	9 4	wex	|- E. y A. x ( ph -> x = y )
11	10 3	wal	|- A. z E. y A. x ( ph -> x = y )
12	2 11	wb	|- ( E** x ph <-> A. z E. y A. x ( ph -> x = y ) )