Theorem mo

Description: Equivalent definitions of "there exists at most one". (Contributed by NM, 7-Aug-1994) (Revised by Mario Carneiro, 7-Oct-2016) (Proof shortened by Wolf Lammen, 2-Dec-2018)

	Ref	Expression
Hypothesis	mo.nf	⊢ Ⅎ 𝑦 𝜑
Assertion	mo	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		mo.nf	⊢ Ⅎ 𝑦 𝜑
2	1	mof	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
3	1	mo3	⊢ ( ∃* 𝑥 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
4	2 3	bitr3i	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )