Bound-variable hypothesis builder for the at-most-one quantifier. See nfmo for a version without disjoint variable conditions but requiring [ax-13]. (Contributed by NM, 9-Mar-1995.) (Revised by Wolf Lammen, 2-Oct-2023.)
Bound-variable hypothesis builder for the at-most-one quantifier. See nfmo for a version without disjoint variable conditions but requiring [ax-13]. (Contributed by NM, 9-Mar-1995.) (Revised by Wolf Lammen, 2-Oct-2023.)