Metamath Proof Explorer

Theorem rals-no-surprise

Description: Demonstrate that there is never a "surprise" when using the allsome quantifier restricted to a class, that is, it is never possible for the consequent to be both always true and always false of the members of A that satisfy the antecedent. This is the restricted counterpart of als-no-surprise , and follows from it by dfrals2 . Note that this needs no assumption that A is nonempty, because allsome requires a member of A satisfying ph , and that member would have to satisfy both ps and -. ps . The ordinary restricted "for all" requires no such member and can be vacuously true, as shown in empty-surprise2 ; that is the point of allsome. (Contributed by David A. Wheeler, 12-Jul-2026)

Ref Expression
Assertion rals-no-surprise ⊢ ¬ ∀∃ x ∈ A φ → ψ ∧ ∀∃ x ∈ A φ → ¬ ψ

Proof

Step Hyp Ref Expression
1 als-no-surprise ⊢ ¬ ∀∃ x x ∈ A ∧ φ → ψ ∧ ∀∃ x x ∈ A ∧ φ → ¬ ψ
2 dfrals2 ⊢ ∀∃ x ∈ A φ → ψ ↔ ∀∃ x x ∈ A ∧ φ → ψ
3 dfrals2 ⊢ ∀∃ x ∈ A φ → ¬ ψ ↔ ∀∃ x x ∈ A ∧ φ → ¬ ψ
4 2 3 anbi12i ⊢ ∀∃ x ∈ A φ → ψ ∧ ∀∃ x ∈ A φ → ¬ ψ ↔ ∀∃ x x ∈ A ∧ φ → ψ ∧ ∀∃ x x ∈ A ∧ φ → ¬ ψ
5 1 4 mtbir ⊢ ¬ ∀∃ x ∈ A φ → ψ ∧ ∀∃ x ∈ A φ → ¬ ψ