Metamath Proof Explorer

Theorem nfre1

Description: The setvar x is not free in E. x e. A ph . (Contributed by NM, 19-Mar-1997) (Revised by Mario Carneiro, 7-Oct-2016)

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

Proof

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