Theorem nfe1 2154

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 2147	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
2	1	nf5i 2150	1 ⊢ Ⅎ𝑥∃𝑥𝜑

Syntax hints:  ∃wex 1780  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-10 2145

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfa1  2155  nfnf1  2158  nf6  2291  exdistrf  2469  nfeu1ALT  2675  euor2  2697  2moexv  2712  moexexvw  2713  2moswapv  2714  2euexv  2716  eupicka  2719  mopick2  2722  moexex  2723  2moex  2725  2euex  2726  2moswap  2729  2mo  2733  2eu7  2743  2eu8  2744  nfre1  3308  ceqsexg  3648  morex  3712  intab  4908  nfopab1  5137  nfopab2  5138  axrep1  5193  axrep2  5195  axrep3  5196  axrep4  5197  eusv2nf  5298  copsexgw  5383  copsexg  5384  copsex2t  5385  copsex2g  5386  mosubopt  5402  dfid3  5464  dmcoss  5844  imadif  6440  oprabidw  7189  nfoprab1  7217  nfoprab2  7218  nfoprab3  7219  fsplitOLD  7815  zfcndrep  10038  zfcndpow  10040  zfcndreg  10041  zfcndinf  10042  reclem2pr  10472  ex-natded9.26  28200  brabgaf  30361  bnj607  32190  bnj849  32199  bnj1398  32308  bnj1449  32322  finminlem  33668  exisym1  33774  bj-alexbiex  34035  bj-exexbiex  34036  bj-biexal2  34042  bj-biexex  34045  bj-sbf3  34164  copsex2d  34433  sbexi  35393  ac6s6  35452  e2ebind  40904  e2ebindVD  41253  e2ebindALT  41270  stoweidlem57  42349  ovncvrrp  42853  ich2ex  43636  ichreuopeq  43642  reuopreuprim  43695