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	|- F/ x ph
	nfalseu.2	|- F/ x ps
Assertion	nfalseu	|- F/ x AE! y ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		nfalseu.1	|- F/ x ph
2		nfalseu.2	|- F/ x ps
3		df-alseu	|- ( AE! y ( ph -> ps ) <-> ( A. y ( ph -> ps ) /\ E! y ph ) )
4	1 2	nfim	|- F/ x ( ph -> ps )
5	4	nfal	|- F/ x A. y ( ph -> ps )
6	1	nfeuw	|- F/ x E! y ph
7	5 6	nfan	|- F/ x ( A. y ( ph -> ps ) /\ E! y ph )
8	3 7	nfxfr	|- F/ x AE! y ( ph -> ps )