Theorem nfalseu

Description: Bound-variable hypothesis builder for "all some one". This is the "all some one" counterpart of nfals . Unlike nfals it requires x and y to be disjoint, because the corresponding builder for E! is nfeuw , which requires it; the version without that requirement, nfeu , depends on ax-13 and its use is discouraged. (Contributed by David A. Wheeler, 21-Jul-2026)

	Ref	Expression
Hypotheses	nfalseu.1	$$⊢Ⅎx\phi$$
	nfalseu.2	$$⊢Ⅎx\psi$$
Assertion	nfalseu	$$⊢Ⅎx\forall \exists !y\left(\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfalseu.1	$$⊢Ⅎx\phi$$
2		nfalseu.2	$$⊢Ⅎx\psi$$
3		df-alseu	$$⊢\forall \exists !y\left(\phi \to \psi \right)\leftrightarrow \left(\forall y\left(\phi \to \psi \right)\wedge \exists !y\phi \right)$$
4	1 2	nfim	$$⊢Ⅎx\left(\phi \to \psi \right)$$
5	4	nfal	$$⊢Ⅎx\forall y\left(\phi \to \psi \right)$$
6	1	nfeuw	$$⊢Ⅎx\exists !y\phi$$
7	5 6	nfan	$$⊢Ⅎx\left(\forall y\left(\phi \to \psi \right)\wedge \exists !y\phi \right)$$
8	3 7	nfxfr	$$⊢Ⅎx\forall \exists !y\left(\phi \to \psi \right)$$