Theorem nfals

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

	Ref	Expression
Hypotheses	nfals.1	|- F/ x ph
	nfals.2	|- F/ x ps
Assertion	nfals	|- F/ x AE y ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		nfals.1	|- F/ x ph
2		nfals.2	|- F/ x ps
3		df-als	|- ( 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	nfex	|- 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 )