Description: Extend wff definition to include "all some one" applied to a top-level implication, which means ps is true whenever ph is true, and exactly one x satisfies ph . (Contributed by David A. Wheeler, 21-Jul-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | walseu | wff AE! x ( ph -> ps ) |