Definition df-bj-mo 34760

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

Assertion

Ref	Expression
df-bj-mo	⊢ (∃**𝑥𝜑 ↔ ∀𝑧∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))

Distinct variable groups:   𝑥,𝑦,𝑧   𝜑,𝑦,𝑧

Allowed substitution hint:   𝜑(𝑥)

Detailed syntax breakdown of Definition df-bj-mo

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3	1, 2	wmoo 34759	. 2 wff ∃**𝑥𝜑
4		vy	. . . . . . 7 setvar 𝑦
5	2, 4	weq 1967	. . . . . 6 wff 𝑥 = 𝑦
6	1, 5	wi 4	. . . . 5 wff (𝜑 → 𝑥 = 𝑦)
7	6, 2	wal 1537	. . . 4 wff ∀𝑥(𝜑 → 𝑥 = 𝑦)
8	7, 4	wex 1783	. . 3 wff ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)
9		vz	. . 3 setvar 𝑧
10	8, 9	wal 1537	. 2 wff ∀𝑧∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)
11	3, 10	wb 205	1 wff (∃**𝑥𝜑 ↔ ∀𝑧∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))

This definition is referenced by: (None)