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 ( ∃** 𝑥 𝜑 ↔ ∀ 𝑧𝑦𝑥 ( 𝜑𝑥 = 𝑦 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx 𝑥
1 wph 𝜑
2 1 0 wmoo ∃** 𝑥 𝜑
3 vz 𝑧
4 vy 𝑦
5 0 cv 𝑥
6 4 cv 𝑦
7 5 6 wceq 𝑥 = 𝑦
8 1 7 wi ( 𝜑𝑥 = 𝑦 )
9 8 0 wal 𝑥 ( 𝜑𝑥 = 𝑦 )
10 9 4 wex 𝑦𝑥 ( 𝜑𝑥 = 𝑦 )
11 10 3 wal 𝑧𝑦𝑥 ( 𝜑𝑥 = 𝑦 )
12 2 11 wb ( ∃** 𝑥 𝜑 ↔ ∀ 𝑧𝑦𝑥 ( 𝜑𝑥 = 𝑦 ) )