Theorem nfe1 1789

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

Syntax hints:   E.wex 1596   F/wnf 1599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-10 1786

This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600

This theorem is referenced by:  nf3  1910  exdistrf  2048  nfmo1  2289  euor2  2334  euor2OLD  2335  euanOLD  2354  eupicka  2365  mopick2  2370  moexex  2371  moexexOLD  2372  2moex  2374  2euex  2375  2moswap  2378  2mo  2382  2moOLD  2383  2eu4OLD  2391  2eu7  2395  2eu8  2396  nfre1  2925  ceqsexg  3235  morex  3287  sbc6g  3357  intab  4312  nfopab1  4513  nfopab2  4514  axrep1  4559  axrep2  4560  axrep3  4561  axrep4  4562  eusv2nf  4645  copsexg  4732  copsexgOLD  4733  copsex2t  4734  copsex2g  4735  mosubopt  4745  dfid3  4796  dmcoss  5262  imadif  5663  nfoprab1  6330  nfoprab2  6331  nfoprab3  6332  fsplit  6888  zfcndrep  8992  zfcndpow  8994  zfcndreg  8995  zfcndinf  8996  reclem2pr  9426  ex-natded9.26  24845  exisym1  29494  finminlem  29741  sbexi  30147  sbcexf  30149  ac6s6  30212  stoweidlem57  31385  e2ebind  32434  e2ebindVD  32810  e2ebindALT  32827  bnj607  33071  bnj849  33080  bnj1398  33187  bnj1449  33201  bj-alexbiex  33353  bj-exexbiex  33354  bj-biexal2  33360  bj-biexex  33363  bj-axrep1  33473  bj-axrep2  33474  bj-axrep3  33475  bj-axrep4  33476  bj-sbf3  33509