Metamath Proof Explorer


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 ** x φ z y x φ x = y

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvar x
1 wph wff φ
2 1 0 wmoo wff ** x φ
3 vz setvar z
4 vy setvar y
5 0 cv setvar x
6 4 cv setvar y
7 5 6 wceq wff x = y
8 1 7 wi wff φ x = y
9 8 0 wal wff x φ x = y
10 9 4 wex wff y x φ x = y
11 10 3 wal wff z y x φ x = y
12 2 11 wb wff ** x φ z y x φ x = y