Bound-variable hypothesis builder for the unique existential quantifier. Version of nfeu with a disjoint variable condition, which does not require [ax-13]. (Contributed by NM, 8-Mar-1995.) Avoid [ax-13]. (Revised by GG, 10-Jan-2024.)
Bound-variable hypothesis builder for the unique existential quantifier. Version of nfeu with a disjoint variable condition, which does not require [ax-13]. (Contributed by NM, 8-Mar-1995.) Avoid [ax-13]. (Revised by GG, 10-Jan-2024.)