Theorem nfe1 1841

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

Syntax hints:   E.wex 1613   F/wnf 1617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-10 1838

This theorem depends on definitions:  df-bi 185  df-ex 1614  df-nf 1618

This theorem is referenced by:  nf3  1962  exdistrf  2076  nfmo1  2296  euor2  2334  eupicka  2359  mopick2  2362  moexex  2363  2moex  2365  2euex  2366  2moswap  2369  2mo  2373  2moOLD  2374  2eu4OLD  2381  2eu7  2385  2eu8  2386  nfre1  2918  ceqsexg  3231  morex  3283  intab  4319  nfopab1  4523  nfopab2  4524  axrep1  4569  axrep2  4570  axrep3  4571  axrep4  4572  eusv2nf  4654  copsexg  4741  copsexgOLD  4742  copsex2t  4743  copsex2g  4744  mosubopt  4754  dfid3  4805  dmcoss  5272  imadif  5669  nfoprab1  6345  nfoprab2  6346  nfoprab3  6347  fsplit  6904  zfcndrep  9009  zfcndpow  9011  zfcndreg  9012  zfcndinf  9013  reclem2pr  9443  ex-natded9.26  25267  brabgaf  27604  exisym1  30094  finminlem  30341  sbexi  30721  ac6s6  30785  stoweidlem57  32042  e2ebind  33479  e2ebindVD  33855  e2ebindALT  33872  bnj607  34117  bnj849  34126  bnj1398  34233  bnj1449  34247  bj-alexbiex  34396  bj-exexbiex  34397  bj-biexal2  34403  bj-biexex  34406  bj-axrep1  34517  bj-axrep2  34518  bj-axrep3  34519  bj-axrep4  34520  bj-sbf3  34553