Metamath Proof Explorer

Theorem dfalseu2

Description: An "all some one" statement is equivalent to its universal part conjoined with the claim that exactly one x satisfies both ph and ps . In other words, given A. x ( ph -> ps ) , requiring exactly one x to satisfy ph , which is what df-alseu requires, and requiring exactly one x to satisfy ( ph /\ ps ) come to the same thing. Read ph as "is a king" and ps as "is hungry": if every king is hungry, then "there is exactly one king" and "there is exactly one hungry king" say the same thing, so either of them, together with "every king is hungry", gives "the king is hungry".

The universal conjunct is what makes that work, and it cannot be dropped. E! x ( ph /\ ps ) on its own is strictly weaker than AE! x ( ph -> ps ) , since it is satisfied when many things are ph and just one of those is ps , as in a region with five kings exactly one of whom is hungry; see alseueu for the one direction that does hold without it. Uniqueness attaches to the antecedent, not to the conjunction. Russell's analysis of a definite description is built the same way: its uniqueness clause constrains the description predicate alone, while the predication is a separate conjunct. See his worked example of "the father of Charles II was executed", Russell1905 p. 482. (Contributed by David A. Wheeler, 21-Jul-2026)

Ref Expression
Assertion dfalseu2 ⊢ ∀∃! x φ → ψ ↔ ∀ x φ → ψ ∧ ∃! x φ ∧ ψ

Proof

Step Hyp Ref Expression
1 df-alseu ⊢ ∀∃! x φ → ψ ↔ ∀ x φ → ψ ∧ ∃! x φ
2 pm4.71 ⊢ φ → ψ ↔ φ ↔ φ ∧ ψ
3 2 albii ⊢ ∀ x φ → ψ ↔ ∀ x φ ↔ φ ∧ ψ
4 eubi ⊢ ∀ x φ ↔ φ ∧ ψ → ∃! x φ ↔ ∃! x φ ∧ ψ
5 3 4 sylbi ⊢ ∀ x φ → ψ → ∃! x φ ↔ ∃! x φ ∧ ψ
6 5 pm5.32i ⊢ ∀ x φ → ψ ∧ ∃! x φ ↔ ∀ x φ → ψ ∧ ∃! x φ ∧ ψ
7 1 6 bitri ⊢ ∀∃! x φ → ψ ↔ ∀ x φ → ψ ∧ ∃! x φ ∧ ψ