This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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