Theorem nfe1 1777

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

Syntax hints:   E.wex 1589   F/wnf 1592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-10 1774

This theorem depends on definitions:  df-bi 185  df-ex 1590  df-nf 1593

This theorem is referenced by:  nf3  1887  exdistrf  2024  nfmo1  2265  euor2  2307  euor2OLD  2308  euanOLD  2329  eupicka  2339  mopick2  2344  moexex  2345  moexexOLD  2346  2moex  2348  2euex  2349  2moswap  2352  2eu4  2361  2eu7  2364  2eu8  2365  nfre1  2762  ceqsexg  3080  morex  3132  sbc6g  3200  intab  4146  nfopab1  4346  nfopab2  4347  axrep1  4392  axrep2  4393  axrep3  4394  axrep4  4395  eusv2nf  4478  copsexg  4564  copsexgOLD  4565  copsex2t  4566  copsex2g  4567  mosubopt  4577  dfid3  4624  dmcoss  5086  imadif  5481  nfoprab1  6124  nfoprab2  6125  nfoprab3  6126  fsplit  6666  zfcndrep  8768  zfcndpow  8770  zfcndreg  8771  zfcndinf  8772  reclem2pr  9204  ex-natded9.26  23448  exisym1  28117  finminlem  28354  sbexi  28760  sbcexf  28762  ac6s6  28826  stoweidlem57  29695  e2ebind  30970  e2ebindVD  31347  e2ebindALT  31364  bnj607  31608  bnj849  31617  bnj1398  31724  bnj1449  31738  bj-axrep1  31926  bj-axrep2  31927  bj-axrep3  31928  bj-axrep4  31929  bj-sbf3  31962