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 x x φ

Proof

Step Hyp Ref Expression
1 hbe1 x φ x x φ
2 1 nf5i x x φ