Theorem nfe1 2153

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 2146	. 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
2	1	nf5i 2149	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 2144

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

This theorem is referenced by:  nfa1  2154  nfnf1  2157  sbalex  2245  nf6  2285  exdistrf  2447  nfeu1ALT  2584  euor2  2608  2moexv  2622  moexexvw  2623  2moswapv  2624  2euexv  2626  eupicka  2629  mopick2  2632  moexex  2633  2moex  2635  2euex  2636  2moswap  2639  2mo  2643  2eu7  2653  2eu8  2654  nfre1  3257  ceqsexg  3603  morex  3673  intab  4926  nfopab1  5159  nfopab2  5160  axrep1  5216  axrep2  5218  axrep3  5219  axrep4OLD  5222  eusv2nf  5331  copsexgw  5428  copsexg  5429  copsex2t  5430  mosubopt  5448  dfid3  5512  dmcossOLD  5914  imadif  6565  oprabidw  7377  nfoprab1  7407  nfoprab2  7408  nfoprab3  7409  zfcndrep  10505  zfcndpow  10507  zfcndreg  10508  zfcndinf  10509  reclem2pr  10939  ex-natded9.26  30399  brabgaf  32589  bnj607  34928  bnj849  34937  bnj1398  35046  bnj1449  35060  finminlem  36360  exisym1  36466  bj-alexbiex  36741  bj-exexbiex  36742  bj-biexal2  36748  bj-biexex  36751  bj-sbf3  36881  copsex2d  37181  sbexi  38161  ac6s6  38220  e2ebind  44604  e2ebindVD  44952  e2ebindALT  44969  stoweidlem57  46103  ovncvrrp  46610  ich2ex  47507  ichreuopeq  47512  reuopreuprim  47565  pgind  49757