Theorem nfe1 2067

Description: The setvar 𝑥 is not free in ∃𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfe1	⊢ Ⅎ𝑥∃𝑥𝜑

Proof of Theorem nfe1

Step	Hyp	Ref	Expression
1		hbe1 2061	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
2	1	nf5i 2064	1 ⊢ Ⅎ𝑥∃𝑥𝜑

Syntax hints:  ∃wex 1744  Ⅎwnf 1748

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

This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750

This theorem is referenced by:  nfa1  2068  nfnf1  2071  nf6  2155  exdistrf  2364  nfmo1  2509  euor2  2543  eupicka  2566  mopick2  2569  moexex  2570  2moex  2572  2euex  2573  2moswap  2576  2mo  2580  2eu7  2588  2eu8  2589  nfre1  3034  ceqsexg  3365  morex  3423  intab  4539  nfopab1  4752  nfopab2  4753  axrep1  4805  axrep2  4806  axrep3  4807  axrep4  4808  eusv2nf  4894  copsexg  4985  copsex2t  4986  copsex2g  4987  mosubopt  5001  dfid3  5054  dmcoss  5417  imadif  6011  nfoprab1  6746  nfoprab2  6747  nfoprab3  6748  fsplit  7327  zfcndrep  9474  zfcndpow  9476  zfcndreg  9477  zfcndinf  9478  reclem2pr  9908  ex-natded9.26  27406  brabgaf  29546  bnj607  31112  bnj849  31121  bnj1398  31228  bnj1449  31242  finminlem  32437  exisym1  32548  bj-alexbiex  32815  bj-exexbiex  32816  bj-biexal2  32822  bj-biexex  32825  bj-axrep1  32913  bj-axrep2  32914  bj-axrep3  32915  bj-axrep4  32916  bj-sbf3  32951  sbexi  34046  ac6s6  34110  e2ebind  39096  e2ebindVD  39462  e2ebindALT  39479  stoweidlem57  40592  ovncvrrp  41099