Theorem nfe1 1935

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

Syntax hints:   E.wex 1671   F/wnf 1675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-10 1932

This theorem depends on definitions:  df-bi 190  df-ex 1672  df-nf 1676

This theorem is referenced by:  nf3  2061  exdistrf  2182  nfmo1  2330  euor2  2363  eupicka  2386  mopick2  2389  moexex  2390  2moex  2392  2euex  2393  2moswap  2396  2mo  2400  2eu7  2408  2eu8  2409  nfre1  2846  ceqsexg  3158  morex  3210  intab  4256  nfopab1  4462  nfopab2  4463  axrep1  4509  axrep2  4510  axrep3  4511  axrep4  4512  eusv2nf  4599  copsexg  4687  copsex2t  4688  copsex2g  4689  mosubopt  4699  dfid3  4755  dmcoss  5100  imadif  5668  nfoprab1  6359  nfoprab2  6360  nfoprab3  6361  fsplit  6920  zfcndrep  9057  zfcndpow  9059  zfcndreg  9060  zfcndinf  9061  reclem2pr  9491  ex-natded9.26  25948  brabgaf  28292  bnj607  29799  bnj849  29808  bnj1398  29915  bnj1449  29929  finminlem  31045  exisym1  31155  bj-alexbiex  31359  bj-exexbiex  31360  bj-biexal2  31366  bj-biexex  31369  bj-axrep1  31469  bj-axrep2  31470  bj-axrep3  31471  bj-axrep4  31472  bj-sbf3  31507  sbexi  32415  ac6s6  32479  e2ebind  37000  e2ebindVD  37372  e2ebindALT  37389  stoweidlem57  38030  ovncvrrp  38504