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

Metamath Proof Explorer

Theorem nfe1

Description: The setvar x is not free in E. x ph . (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Assertion nfe1 
|- F/ x E. x ph

Proof

Step Hyp Ref Expression
1 hbe1 
 |-  ( E. x ph -> A. x E. x ph )
2 1 nf5i 
 |-  F/ x E. x ph