Theorem nfe1 1864

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

Syntax hints:   E.wex 1633   F/wnf 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-10 1861

This theorem depends on definitions:  df-bi 185  df-ex 1634  df-nf 1638

This theorem is referenced by:  nf3  1989  exdistrf  2101  nfmo1  2251  euor2  2286  eupicka  2310  mopick2  2313  moexex  2314  2moex  2316  2euex  2317  2moswap  2320  2mo  2324  2moOLD  2325  2eu4OLD  2332  2eu7  2336  2eu8  2337  nfre1  2864  ceqsexg  3180  morex  3232  intab  4257  nfopab1  4460  nfopab2  4461  axrep1  4507  axrep2  4508  axrep3  4509  axrep4  4510  eusv2nf  4591  copsexg  4675  copsex2t  4676  copsex2g  4677  mosubopt  4687  dfid3  4738  dmcoss  5082  imadif  5643  nfoprab1  6326  nfoprab2  6327  nfoprab3  6328  fsplit  6888  zfcndrep  9021  zfcndpow  9023  zfcndreg  9024  zfcndinf  9025  reclem2pr  9455  ex-natded9.26  25544  brabgaf  27884  bnj607  29288  bnj849  29297  bnj1398  29404  bnj1449  29418  finminlem  30533  exisym1  30643  bj-alexbiex  30804  bj-exexbiex  30805  bj-biexal2  30811  bj-biexex  30814  bj-axrep1  30925  bj-axrep2  30926  bj-axrep3  30927  bj-axrep4  30928  bj-sbf3  30961  sbexi  31778  ac6s6  31842  e2ebind  36340  e2ebindVD  36723  e2ebindALT  36740  stoweidlem57  37188