Theorem nexmo

Description: Nonexistence implies uniqueness. (Contributed by BJ, 30-Sep-2022) Avoid ax-11 . (Revised by Wolf Lammen, 16-Oct-2022)

	Ref	Expression
Assertion	nexmo	⊢ ( ¬ ∃ 𝑥 𝜑 → ∃* 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → 𝑥 = 𝑦 ) )
2	1	alimi	⊢ ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
3	2	alrimiv	⊢ ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
4	3	19.2d	⊢ ( ∀ 𝑥 ¬ 𝜑 → ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
5		alnex	⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
6	5	bicomi	⊢ ( ¬ ∃ 𝑥 𝜑 ↔ ∀ 𝑥 ¬ 𝜑 )
7		dfmo	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
8	4 6 7	3imtr4i	⊢ ( ¬ ∃ 𝑥 𝜑 → ∃* 𝑥 𝜑 )