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, 10-Jan-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		nfcvd	|- ( ph -> F/_ x y )
6	5 2	nfeld	|- ( ph -> F/ x y e. A )
7	6 3	nfimd	|- ( ph -> F/ x ( y e. A -> ps ) )
8	1 7	nfald	|- ( ph -> F/ x A. y ( y e. A -> ps ) )
9	4 8	nfxfrd	|- ( ph -> F/ x A. y e. A ps )