Theorem nfe1 2185

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

Syntax hints:  ∃wex 1809  Ⅎwnf 1813

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

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814

This theorem is referenced by:  nfa1  2186  nfnf1  2189  sbalex  2278  nf6  2318  exdistrf  2479  nfeu1  2617  euor2  2641  2moexv  2655  moexexvw  2656  2moswapv  2657  2euexv  2659  eupicka  2662  mopick2  2665  moexex  2666  2moex  2668  2euex  2669  2moswap  2672  2mo  2676  2eu7  2685  2eu8  2686  nfre1  3290  ceqsexg  3612  morex  3682  intab  4943  nfopab1  5181  nfopab2  5182  axrep1  5239  axrep2  5241  axrep3  5242  axrep4OLD  5245  eusv2nf  5366  copsexgwOLD  5473  copsexg  5474  copsex2t  5475  mosubopt  5493  dfid3  5559  dmcossOLD  5966  imadif  6620  oprabidw  7441  nfoprab1  7471  nfoprab2  7472  nfoprab3  7473  zfcndrep  10594  zfcndpow  10596  zfcndreg  10597  zfcndinf  10598  reclem2pr  11028  ex-natded9.26  30770  brabgaf  32951  bnj607  35304  bnj849  35313  bnj1398  35422  bnj1449  35436  finminlem  36829  exisym1  36935  bj-alexbiex  37324  bj-exexbiex  37325  bj-biexal2  37331  bj-biexex  37334  bj-sbf3  37474  bj-axseprep  37711  bj-axreprepsep  37712  copsex2d  37783  sbexi  38762  ac6s6  38821  nfe2  42984  e2ebind  45272  e2ebindVD  45620  e2ebindALT  45637  stoweidlem57  46771  ovncvrrp  47278  ich2ex  48217  ichreuopeq  48222  reuopreuprim  48275  pgind  50495