Theorem eunex

Description: Existential uniqueness implies there is a value for which the wff argument is false. (Contributed by NM, 24-Oct-2010) (Proof shortened by BJ, 2-Jan-2023)

	Ref	Expression
Assertion	eunex	⊢ ( ∃! 𝑥 𝜑 → ∃ 𝑥 ¬ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		dtru	⊢ ¬ ∀ 𝑥 𝑥 = 𝑦
2		albi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝑥 = 𝑦 ) )
3	1 2	mtbiri	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ¬ ∀ 𝑥 𝜑 )
4	3	exlimiv	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ¬ ∀ 𝑥 𝜑 )
5		eu6	⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
6		exnal	⊢ ( ∃ 𝑥 ¬ 𝜑 ↔ ¬ ∀ 𝑥 𝜑 )
7	4 5 6	3imtr4i	⊢ ( ∃! 𝑥 𝜑 → ∃ 𝑥 ¬ 𝜑 )