Theorem nfe1 2144

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

Syntax hints:  ∃wex 1823  Ⅎwnf 1827

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-10 2135

This theorem depends on definitions:  df-bi 199  df-ex 1824  df-nf 1828

This theorem is referenced by:  nfa1  2145  nfnf1  2148  nf6  2257  exdistrf  2413  nfeu1ALT  2610  nfmo1OLD  2622  euor2  2648  eupicka  2664  mopick2  2667  moexex  2668  2moex  2670  2euex  2671  2moswap  2674  2mo  2678  2eu7  2688  2eu8  2689  nfre1  3186  ceqsexg  3537  morex  3602  intab  4742  nfopab1  4957  nfopab2  4958  axrep1  5009  axrep2  5011  axrep3  5012  axrep4  5013  eusv2nf  5109  copsexg  5189  copsex2t  5190  copsex2g  5191  mosubopt  5209  dfid3  5264  dmcoss  5633  imadif  6220  nfoprab1  6983  nfoprab2  6984  nfoprab3  6985  fsplit  7565  zfcndrep  9773  zfcndpow  9775  zfcndreg  9776  zfcndinf  9777  reclem2pr  10207  ex-natded9.26  27868  brabgaf  30000  bnj607  31593  bnj849  31602  bnj1398  31709  bnj1449  31723  finminlem  32909  exisym1  33014  bj-alexbiex  33286  bj-exexbiex  33287  bj-biexal2  33293  bj-biexex  33296  bj-axrep1  33373  bj-axrep2  33374  bj-axrep3  33375  bj-axrep4  33376  bj-sbf3  33409  sbexi  34548  ac6s6  34612  e2ebind  39737  e2ebindVD  40095  e2ebindALT  40112  stoweidlem57  41215  ovncvrrp  41719