Theorem nfe1 1426

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 1425	. 2 |- ( E. x ph -> A. x E. x ph )
2	1	nfi 1392	1 |- F/ x E. x ph

Syntax hints:   F/wnf 1390   E.wex 1422

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1379  ax-ie1 1423

This theorem depends on definitions:  df-bi 115  df-nf 1391

This theorem is referenced by:  nf3  1600  sb4or  1756  nfmo1  1955  euexex  2028  2moswapdc  2033  nfre1  2413  ceqsexg  2733  morex  2787  sbc6g  2850  rgenm  3365  intab  3691  nfopab1  3873  nfopab2  3874  copsexg  4034  copsex2t  4035  copsex2g  4036  eusv2nf  4241  onintonm  4296  mosubopt  4460  dmcoss  4659  imadif  5046  funimaexglem  5049  nfoprab1  5632  nfoprab2  5633  nfoprab3  5634  exmidfodomrlemr  6730  exmidfodomrlemrALT  6731