Theorem nfrmod

Description: Deduction version of nfrmo . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 17-Jun-2017) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nfreud.1	|- F/ y ph
2		nfreud.2	|- ( ph -> F/_ x A )
3		nfreud.3	|- ( ph -> F/ x ps )
4		df-rmo	|- ( 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	nfmod2	|- ( ph -> F/ x E* y ( y e. A /\ ps ) )
12	4 11	nfxfrd	|- ( ph -> F/ x E* y e. A ps )