Theorem nfraldw

Description: Deduction version of nfralw . Version of nfrald with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 15-Feb-2013) (Revised by Gino Giotto, 24-Sep-2024)

	Ref	Expression
Hypotheses	nfraldw.1	|- F/ y ph
	nfraldw.2	|- ( ph -> F/_ x A )
	nfraldw.3	|- ( ph -> F/ x ps )
Assertion	nfraldw	|- ( ph -> F/ x A. y e. A ps )

Proof

Step	Hyp	Ref	Expression
1		nfraldw.1	|- F/ y ph
2		nfraldw.2	|- ( ph -> F/_ x A )
3		nfraldw.3	|- ( ph -> F/ x ps )
4		df-ral	|- ( A. y e. A ps <-> A. y ( y e. A -> ps ) )
5	2	nfcrd	|- ( ph -> F/ x y e. A )
6	5 3	nfimd	|- ( ph -> F/ x ( y e. A -> ps ) )
7	1 6	nfald	|- ( ph -> F/ x A. y ( y e. A -> ps ) )
8	4 7	nfxfrd	|- ( ph -> F/ x A. y e. A ps )