Theorem nfe1 2014

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

Syntax hints:  ∃wex 1695  Ⅎwnf 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-10 2006

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701

This theorem is referenced by:  nfa1  2015  nfnf1  2018  nf6  2103  exdistrf  2321  nfmo1  2469  euor2  2502  eupicka  2525  mopick2  2528  moexex  2529  2moex  2531  2euex  2532  2moswap  2535  2mo  2539  2eu7  2547  2eu8  2548  nfre1  2988  ceqsexg  3304  morex  3357  intab  4442  nfopab1  4651  nfopab2  4652  axrep1  4700  axrep2  4701  axrep3  4702  axrep4  4703  eusv2nf  4790  copsexg  4882  copsex2t  4883  copsex2g  4884  mosubopt  4897  dfid3  4954  dmcoss  5306  imadif  5887  nfoprab1  6602  nfoprab2  6603  nfoprab3  6604  fsplit  7169  zfcndrep  9315  zfcndpow  9317  zfcndreg  9318  zfcndinf  9319  reclem2pr  9749  ex-natded9.26  26668  brabgaf  28800  bnj607  30240  bnj849  30249  bnj1398  30356  bnj1449  30370  finminlem  31482  exisym1  31593  bj-alexbiex  31877  bj-exexbiex  31878  bj-biexal2  31884  bj-biexex  31887  bj-axrep1  31976  bj-axrep2  31977  bj-axrep3  31978  bj-axrep4  31979  bj-sbf3  32014  bj-xnex  32245  sbexi  33086  ac6s6  33150  e2ebind  37800  e2ebindVD  38170  e2ebindALT  38187  stoweidlem57  38950  ovncvrrp  39454