Theorem nfe1 1891

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

Syntax hints:   E.wex 1660   F/wnf 1664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-10 1888

This theorem depends on definitions:  df-bi 189  df-ex 1661  df-nf 1665

This theorem is referenced by:  nf3  2018  exdistrf  2131  nfmo1  2278  euor2  2311  eupicka  2334  mopick2  2337  moexex  2338  2moex  2340  2euex  2341  2moswap  2344  2mo  2348  2moOLD  2349  2eu7  2358  2eu8  2359  nfre1  2887  ceqsexg  3204  morex  3256  intab  4284  nfopab1  4488  nfopab2  4489  axrep1  4535  axrep2  4536  axrep3  4537  axrep4  4538  eusv2nf  4620  copsexg  4704  copsex2t  4705  copsex2g  4706  mosubopt  4716  dfid3  4767  dmcoss  5111  imadif  5674  nfoprab1  6352  nfoprab2  6353  nfoprab3  6354  fsplit  6910  zfcndrep  9041  zfcndpow  9043  zfcndreg  9044  zfcndinf  9045  reclem2pr  9475  ex-natded9.26  25861  brabgaf  28212  bnj607  29729  bnj849  29738  bnj1398  29845  bnj1449  29859  finminlem  30973  exisym1  31083  bj-alexbiex  31247  bj-exexbiex  31248  bj-biexal2  31254  bj-biexex  31257  bj-axrep1  31367  bj-axrep2  31368  bj-axrep3  31369  bj-axrep4  31370  bj-sbf3  31403  sbexi  32309  ac6s6  32373  e2ebind  36832  e2ebindVD  37214  e2ebindALT  37231  stoweidlem57  37782  ovncvrrp  38205