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 50642
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 50627 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 50643 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 50627 . 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
This proof depends on syntax axioms:  wi 4  wb 209  wa 400  wal 1568  ∃!weu 2596  ∀∃!walseu 50625
This proof depends on 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 proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-mo 2567  df-eu 2597  df-alseu 50627
This theorem is used by:  alseueu  50643
  Copyright terms: Public domain W3C validator