Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dfalseu2 Structured version   Visualization version   GIF version

Theorem dfalseu2 50614
Description: An "all some one" statement is equivalent to its universal part conjoined with the claim that exactly one 𝑥 satisfies both 𝜑 and 𝜓. In other words, given 𝑥(𝜑𝜓), requiring exactly one 𝑥 to satisfy 𝜑, which is what df-alseu 50599 requires, and requiring exactly one 𝑥 to satisfy (𝜑𝜓) come to the same thing. Read 𝜑 as "is a king" and 𝜓 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. ∃!𝑥(𝜑𝜓) on its own is strictly weaker than ∀∃!𝑥(𝜑𝜓), since it is satisfied when many things are 𝜑 and just one of those is 𝜓, as in a region with five kings exactly one of whom is hungry; see alseueu 50615 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.)

Assertion
Ref Expression
dfalseu2 (∀∃!𝑥(𝜑𝜓) ↔ (∀𝑥(𝜑𝜓) ∧ ∃!𝑥(𝜑𝜓)))

Proof of Theorem dfalseu2
StepHypRef Expression
1 df-alseu 50599 . 2 (∀∃!𝑥(𝜑𝜓) ↔ (∀𝑥(𝜑𝜓) ∧ ∃!𝑥𝜑))
2 pm4.71 566 . . . . 5 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜑𝜓)))
32albii 1849 . . . 4 (∀𝑥(𝜑𝜓) ↔ ∀𝑥(𝜑 ↔ (𝜑𝜓)))
4 eubi 2612 . . . 4 (∀𝑥(𝜑 ↔ (𝜑𝜓)) → (∃!𝑥𝜑 ↔ ∃!𝑥(𝜑𝜓)))
53, 4sylbi 220 . . 3 (∀𝑥(𝜑𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑥(𝜑𝜓)))
65pm5.32i 584 . 2 ((∀𝑥(𝜑𝜓) ∧ ∃!𝑥𝜑) ↔ (∀𝑥(𝜑𝜓) ∧ ∃!𝑥(𝜑𝜓)))
71, 6bitri 278 1 (∀∃!𝑥(𝜑𝜓) ↔ (∀𝑥(𝜑𝜓) ∧ ∃!𝑥(𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 400  wal 1568  ∃!weu 2596  ∀∃!walseu 50597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038
This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-mo 2567  df-eu 2597  df-alseu 50599
This theorem is referenced by:  alseueu  50615
  Copyright terms: Public domain W3C validator