Theorem nfe1 1920

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

Syntax hints:   E.wex 1665   F/wnf 1669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-10 1917

This theorem depends on definitions:  df-bi 189  df-ex 1666  df-nf 1670

This theorem is referenced by:  nf3  2044  exdistrf  2169  nfmo1  2312  euor2  2345  eupicka  2368  mopick2  2371  moexex  2372  2moex  2374  2euex  2375  2moswap  2378  2mo  2382  2eu7  2390  2eu8  2391  nfre1  2850  ceqsexg  3172  morex  3224  intab  4268  nfopab1  4472  nfopab2  4473  axrep1  4519  axrep2  4520  axrep3  4521  axrep4  4522  eusv2nf  4604  copsexg  4690  copsex2t  4691  copsex2g  4692  mosubopt  4702  dfid3  4753  dmcoss  5097  imadif  5663  nfoprab1  6345  nfoprab2  6346  nfoprab3  6347  fsplit  6906  zfcndrep  9044  zfcndpow  9046  zfcndreg  9047  zfcndinf  9048  reclem2pr  9478  ex-natded9.26  25881  brabgaf  28228  bnj607  29739  bnj849  29748  bnj1398  29855  bnj1449  29869  finminlem  30986  exisym1  31096  bj-alexbiex  31305  bj-exexbiex  31306  bj-biexal2  31312  bj-biexex  31315  bj-axrep1  31415  bj-axrep2  31416  bj-axrep3  31417  bj-axrep4  31418  bj-sbf3  31451  sbexi  32363  ac6s6  32427  e2ebind  36941  e2ebindVD  37319  e2ebindALT  37336  stoweidlem57  37928  ovncvrrp  38396