Theorem nfrmo

Description: Bound-variable hypothesis builder for restricted uniqueness. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfrmow when possible. (Contributed by NM, 16-Jun-2017) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfreu.1	|- F/_ x A
	nfreu.2	|- F/ x ph
Assertion	nfrmo	|- F/ x E* y e. A ph

Proof

Step	Hyp	Ref	Expression
1		nfreu.1	|- F/_ x A
2		nfreu.2	|- F/ x ph
3		df-rmo	|- ( E* y e. A ph <-> E* y ( y e. A /\ ph ) )
4		nftru	|- F/ y T.
5		nfcvf	|- ( -. A. x x = y -> F/_ x y )
6	1	a1i	|- ( -. A. x x = y -> F/_ x A )
7	5 6	nfeld	|- ( -. A. x x = y -> F/ x y e. A )
8	2	a1i	|- ( -. A. x x = y -> F/ x ph )
9	7 8	nfand	|- ( -. A. x x = y -> F/ x ( y e. A /\ ph ) )
10	9	adantl	|- ( ( T. /\ -. A. x x = y ) -> F/ x ( y e. A /\ ph ) )
11	4 10	nfmod2	|- ( T. -> F/ x E* y ( y e. A /\ ph ) )
12	11	mptru	|- F/ x E* y ( y e. A /\ ph )
13	3 12	nfxfr	|- F/ x E* y e. A ph