This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 dtruALT2 ⊢ ¬ ∀ 𝑥 𝑥 = 𝑦
2 albi ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝑥 = 𝑦 ) )
3 1 2 mtbiri ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ¬ ∀ 𝑥 𝜑 )
4 3 exlimiv ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ¬ ∀ 𝑥 𝜑 )
5 eu6 ⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
6 exnal ⊢ ( ∃ 𝑥 ¬ 𝜑 ↔ ¬ ∀ 𝑥 𝜑 )
7 4 5 6 3imtr4i ⊢ ( ∃! 𝑥 𝜑 → ∃ 𝑥 ¬ 𝜑 )