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 50671
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 50656 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 50672 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 50656 . 2 (∀∃!𝑥(𝜑𝜓) ↔ (∀𝑥(𝜑𝜓) ∧ ∃!𝑥𝜑))
2 pm4.71 567 . . . . 5 ((𝜑𝜓) ↔ (𝜑 ↔ (𝜑𝜓)))
32albii 1852 . . . 4 (∀𝑥(𝜑𝜓) ↔ ∀𝑥(𝜑 ↔ (𝜑𝜓)))
4 eubi 2614 . . . 4 (∀𝑥(𝜑 ↔ (𝜑𝜓)) → (∃!𝑥𝜑 ↔ ∃!𝑥(𝜑𝜓)))
53, 4sylbi 220 . . 3 (∀𝑥(𝜑𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑥(𝜑𝜓)))
65pm5.32i 585 . 2 ((∀𝑥(𝜑𝜓) ∧ ∃!𝑥𝜑) ↔ (∀𝑥(𝜑𝜓) ∧ ∃!𝑥(𝜑𝜓)))
71, 6bitri 278 1 (∀∃!𝑥(𝜑𝜓) ↔ (∀𝑥(𝜑𝜓) ∧ ∃!𝑥(𝜑𝜓)))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  wb 209  wa 401  wal 1568  ∃!weu 2598  ∀∃!walseu 50654
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041
This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2569  df-eu 2599  df-alseu 50656
This theorem is used by:  alseueu  50672
  Copyright terms: Public domain W3C validator