Metamath Proof Explorer

Theorem nfreu1

Description: The setvar x is not free in E! x e. A ph . (Contributed by NM, 19-Mar-1997)

Ref Expression
Assertion nfreu1 
|- F/ x E! x e. A ph

Proof

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