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	⊢ Ⅎ 𝑥 𝜑
	nfalseu.2	⊢ Ⅎ 𝑥 𝜓
Assertion	nfalseu	⊢ Ⅎ 𝑥 ∀∃! 𝑦 ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		nfalseu.1	⊢ Ⅎ 𝑥 𝜑
2		nfalseu.2	⊢ Ⅎ 𝑥 𝜓
3		df-alseu	⊢ ( ∀∃! 𝑦 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑦 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑦 𝜑 ) )
4	1 2	nfim	⊢ Ⅎ 𝑥 ( 𝜑 → 𝜓 )
5	4	nfal	⊢ Ⅎ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 )
6	1	nfeuw	⊢ Ⅎ 𝑥 ∃! 𝑦 𝜑
7	5 6	nfan	⊢ Ⅎ 𝑥 ( ∀ 𝑦 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑦 𝜑 )
8	3 7	nfxfr	⊢ Ⅎ 𝑥 ∀∃! 𝑦 ( 𝜑 → 𝜓 )