This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 nfrmo.1 
|- F/_ x A
nfrmo.2 
|- F/ x ph
Assertion nfrmo 
|- F/ x E* y e. A ph

Proof

Step Hyp Ref Expression
1 nfrmo.1 
 |-  F/_ x A
2 nfrmo.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