Theorem nfe1 2191

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

Syntax hints:  ∃wex 1806  Ⅎwnf 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-10 2182

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811

This theorem is referenced by:  nfa1  2192  nfnf1  2195  sbalex  2284  nf6  2324  exdistrf  2485  nfeu1  2623  euor2  2647  2moexv  2661  moexexvw  2662  2moswapv  2663  2euexv  2665  eupicka  2668  mopick2  2671  moexex  2672  2moex  2674  2euex  2675  2moswap  2678  2mo  2682  2eu7  2691  2eu8  2692  nfre1  3296  ceqsexg  3621  morex  3691  intab  4947  nfopab1  5185  nfopab2  5186  axrep1  5243  axrep2  5245  axrep3  5246  axrep4OLD  5249  eusv2nf  5367  copsexgwOLD  5474  copsexg  5475  copsex2t  5476  mosubopt  5494  dfid3  5560  dmcossOLD  5967  imadif  6621  oprabidw  7442  nfoprab1  7472  nfoprab2  7473  nfoprab3  7474  zfcndrep  10598  zfcndpow  10600  zfcndreg  10601  zfcndinf  10602  reclem2pr  11032  ex-natded9.26  30710  brabgaf  32891  bnj607  35248  bnj849  35257  bnj1398  35366  bnj1449  35380  finminlem  36717  exisym1  36823  bj-alexbiex  37212  bj-exexbiex  37213  bj-biexal2  37219  bj-biexex  37222  bj-sbf3  37362  bj-axseprep  37598  bj-axreprepsep  37599  copsex2d  37670  sbexi  38651  ac6s6  38710  nfe2  42873  e2ebind  45163  e2ebindVD  45511  e2ebindALT  45528  stoweidlem57  46662  ovncvrrp  47169  ich2ex  48105  ichreuopeq  48110  reuopreuprim  48163  pgind  50379