Metamath Proof Explorer

Theorem nfrmo1

Description: The setvar x is not free in E* x e. A ph . (Contributed by NM, 16-Jun-2017)

Ref Expression
Assertion nfrmo1 
|- F/ x E* x e. A ph

Proof

Step Hyp Ref Expression
1 df-rmo 
 |-  ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
2 nfmo1 
 |-  F/ x E* x ( x e. A /\ ph )
3 1 2 nfxfr 
 |-  F/ x E* x e. A ph