Theorem nfals

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

	Ref	Expression
Hypotheses	nfals.1	⊢ Ⅎ 𝑥 𝜑
	nfals.2	⊢ Ⅎ 𝑥 𝜓
Assertion	nfals	⊢ Ⅎ 𝑥 ∀∃ 𝑦 ( 𝜑 → 𝜓 )

Proof

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