Description: Extend wff definition to include "all some one" applied to a class, which means ps is true whenever ph is true for x in A , and exactly one x in A satisfies ph . (Contributed by David A. Wheeler, 21-Jul-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wralseu | wff ∀∃! 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) |