Theorem dfalseu2 17151

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 17136 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 A.E! 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 17152 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, 22-Jul-2026.)

Assertion

Ref	Expression
dfalseu2	|- ( A.E! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ( ph /\ ps ) ) )

Proof of Theorem dfalseu2

Step	Hyp	Ref	Expression
1		df-alseu 17136	. 2 |- ( A.E! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ph ) )
2		nfa1 1594	. . . 4 |- F/ x A. x ( ph -> ps )
3		sp 1564	. . . . 5 |- ( A. x ( ph -> ps ) -> ( ph -> ps ) )
4		pm4.71 393	. . . . 5 |- ( ( ph -> ps ) <-> ( ph <-> ( ph /\ ps ) ) )
5	3, 4	sylib 122	. . . 4 |- ( A. x ( ph -> ps ) -> ( ph <-> ( ph /\ ps ) ) )
6	2, 5	eubid 2093	. . 3 |- ( A. x ( ph -> ps ) -> ( E! x ph <-> E! x ( ph /\ ps ) ) )
7	6	pm5.32i 458	. 2 |- ( ( A. x ( ph -> ps ) /\ E! x ph ) <-> ( A. x ( ph -> ps ) /\ E! x ( ph /\ ps ) ) )
8	1, 7	bitri 184	1 |- ( A.E! x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E! x ( ph /\ ps ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1400   E!weu 2086   A.E!walseu 17134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-eu 2089  df-alseu 17136

This theorem is referenced by:  alseueu  17152