Theorem nfrald

Description: Deduction version of nfral . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfraldw when possible. (Contributed by NM, 15-Feb-2013) (Revised by Mario Carneiro, 7-Oct-2016) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nfrald.1	|- F/ y ph
2		nfrald.2	|- ( ph -> F/_ x A )
3		nfrald.3	|- ( ph -> F/ x ps )
4		df-ral	|- ( A. y e. A ps <-> A. y ( y e. A -> ps ) )
5		nfcvf	|- ( -. A. x x = y -> F/_ x y )
6	5	adantl	|- ( ( ph /\ -. A. x x = y ) -> F/_ x y )
7	2	adantr	|- ( ( ph /\ -. A. x x = y ) -> F/_ x A )
8	6 7	nfeld	|- ( ( ph /\ -. A. x x = y ) -> F/ x y e. A )
9	3	adantr	|- ( ( ph /\ -. A. x x = y ) -> F/ x ps )
10	8 9	nfimd	|- ( ( ph /\ -. A. x x = y ) -> F/ x ( y e. A -> ps ) )
11	1 10	nfald2	|- ( ph -> F/ x A. y ( y e. A -> ps ) )
12	4 11	nfxfrd	|- ( ph -> F/ x A. y e. A ps )