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

Metamath Proof Explorer

Definition df-bj-mo

Detailed syntax breakdown