Theorem nfe1 1542

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

Assertion

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

Proof of Theorem nfe1

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

Syntax hints:   F/wnf 1506   E.wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1495  ax-ie1 1539

This theorem depends on definitions:  df-bi 117  df-nf 1507

This theorem is referenced by:  nf3  1715  sb4or  1879  nfmo1  2089  euexex  2163  2moswapdc  2168  nfre1  2573  ceqsexg  2931  morex  2987  sbc6g  3053  intab  3952  nfopab1  4153  nfopab2  4154  copsexg  4330  copsex2t  4331  copsex2g  4332  eusv2nf  4547  onintonm  4609  mosubopt  4784  dmcoss  4994  imadif  5401  funimaexglem  5404  nfoprab1  6053  nfoprab2  6054  nfoprab3  6055  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  dfgrp3mlem  13631