Theorem nfreud

Description: Deduction version of nfreu . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 15-Feb-2013) (Revised by Mario Carneiro, 8-Oct-2016) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nfrmod.1	|- F/ y ph
2		nfrmod.2	|- ( ph -> F/_ x A )
3		nfrmod.3	|- ( ph -> F/ x ps )
4		df-reu	|- ( E! y e. A ps <-> E! 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	nfand	|- ( ( ph /\ -. A. x x = y ) -> F/ x ( y e. A /\ ps ) )
11	1 10	nfeud2	|- ( ph -> F/ x E! y ( y e. A /\ ps ) )
12	4 11	nfxfrd	|- ( ph -> F/ x E! y e. A ps )