Metamath Proof Explorer

Theorem alseu-no-surprise

Description: Demonstrate that there is never a "surprise" when using the "all some one" quantifier, that is, it is never possible for the consequent to be both always true and always false. This follows from als-no-surprise by alseuals . For a contrast, see alimp-surprise . (Contributed by David A. Wheeler, 21-Jul-2026)

Ref Expression
Assertion alseu-no-surprise ⊢ ¬ ∀∃! x φ → ψ ∧ ∀∃! x φ → ¬ ψ

Proof

Step Hyp Ref Expression
1 als-no-surprise ⊢ ¬ ∀∃ x φ → ψ ∧ ∀∃ x φ → ¬ ψ
2 alseuals ⊢ ∀∃! x φ → ψ → ∀∃ x φ → ψ
3 alseuals ⊢ ∀∃! x φ → ¬ ψ → ∀∃ x φ → ¬ ψ
4 2 3 anim12i ⊢ ∀∃! x φ → ψ ∧ ∀∃! x φ → ¬ ψ → ∀∃ x φ → ψ ∧ ∀∃ x φ → ¬ ψ
5 1 4 mto ⊢ ¬ ∀∃! x φ → ψ ∧ ∀∃! x φ → ¬ ψ