Theorem nfralseu

Description: Bound-variable hypothesis builder for "all some one" restricted to a class. This is the "all some one" counterpart of nfrals . (Contributed by David A. Wheeler, 21-Jul-2026)

	Ref	Expression
Hypotheses	nfralseu.1	⊢ Ⅎ 𝑥 𝐴
	nfralseu.2	⊢ Ⅎ 𝑥 𝜑
	nfralseu.3	⊢ Ⅎ 𝑥 𝜓
Assertion	nfralseu	⊢ Ⅎ 𝑥 ∀∃! 𝑦 ∈ 𝐴 ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		nfralseu.1	⊢ Ⅎ 𝑥 𝐴
2		nfralseu.2	⊢ Ⅎ 𝑥 𝜑
3		nfralseu.3	⊢ Ⅎ 𝑥 𝜓
4		df-ralseu	⊢ ( ∀∃! 𝑦 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑦 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑦 ∈ 𝐴 𝜑 ) )
5	2 3	nfim	⊢ Ⅎ 𝑥 ( 𝜑 → 𝜓 )
6	1 5	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐴 ( 𝜑 → 𝜓 )
7	1 2	nfreuw	⊢ Ⅎ 𝑥 ∃! 𝑦 ∈ 𝐴 𝜑
8	6 7	nfan	⊢ Ⅎ 𝑥 ( ∀ 𝑦 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑦 ∈ 𝐴 𝜑 )
9	4 8	nfxfr	⊢ Ⅎ 𝑥 ∀∃! 𝑦 ∈ 𝐴 ( 𝜑 → 𝜓 )