Theorem nfrals

Description: Bound-variable hypothesis builder for "all some" restricted to a class. (Contributed by David A. Wheeler, 12-Jul-2026)

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

Proof

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