Theorem nfe1 1780

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

Syntax hints:   E.wex 1587   F/wnf 1590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-10 1777

This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591

This theorem is referenced by:  nf3  1900  exdistrf  2034  nfmo1  2275  euor2  2320  euor2OLD  2321  euanOLD  2340  eupicka  2351  mopick2  2356  moexex  2357  moexexOLD  2358  2moex  2360  2euex  2361  2moswap  2364  2mo  2368  2moOLD  2369  2eu4OLD  2377  2eu7  2381  2eu8  2382  nfre1  2885  ceqsexg  3192  morex  3244  sbc6g  3314  intab  4261  nfopab1  4461  nfopab2  4462  axrep1  4507  axrep2  4508  axrep3  4509  axrep4  4510  eusv2nf  4593  copsexg  4679  copsexgOLD  4680  copsex2t  4681  copsex2g  4682  mosubopt  4692  dfid3  4740  dmcoss  5202  imadif  5596  nfoprab1  6239  nfoprab2  6240  nfoprab3  6241  fsplit  6782  zfcndrep  8887  zfcndpow  8889  zfcndreg  8890  zfcndinf  8891  reclem2pr  9323  ex-natded9.26  23773  exisym1  28409  finminlem  28656  sbexi  29062  sbcexf  29064  ac6s6  29127  stoweidlem57  29995  e2ebind  31585  e2ebindVD  31961  e2ebindALT  31978  bnj607  32222  bnj849  32231  bnj1398  32338  bnj1449  32352  bj-alexbiex  32502  bj-exexbiex  32503  bj-biexal2  32509  bj-biexex  32512  bj-axrep1  32622  bj-axrep2  32623  bj-axrep3  32624  bj-axrep4  32625  bj-sbf3  32658