MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfe1 Structured version   Visualization version   GIF version

Theorem nfe1 2194
Description: The setvar 𝑥 is not free in 𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfe1 𝑥𝑥𝜑

Proof of Theorem nfe1
StepHypRef Expression
1 hbe1 2187 . 2 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
21nf5i 2190 1 𝑥𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wex 1859  wnf 1863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-10 2185
This theorem depends on definitions:  df-bi 198  df-ex 1860  df-nf 1864
This theorem is referenced by:  nfa1  2195  nfnf1  2198  nf6  2292  exdistrf  2495  nfmo1  2641  euor2  2675  eupicka  2699  mopick2  2702  moexex  2703  2moex  2705  2euex  2706  2moswap  2709  2mo  2713  2eu7  2721  2eu8  2722  nfre1  3190  ceqsexg  3526  morex  3586  intab  4697  nfopab1  4911  nfopab2  4912  axrep1  4963  axrep2  4965  axrep3  4966  axrep4  4967  eusv2nf  5062  copsexg  5143  copsex2t  5144  copsex2g  5145  mosubopt  5163  dfid3  5218  dmcoss  5584  imadif  6182  nfoprab1  6932  nfoprab2  6933  nfoprab3  6934  fsplit  7514  zfcndrep  9719  zfcndpow  9721  zfcndreg  9722  zfcndinf  9723  reclem2pr  10153  ex-natded9.26  27605  brabgaf  29743  bnj607  31307  bnj849  31316  bnj1398  31423  bnj1449  31437  finminlem  32631  exisym1  32738  bj-alexbiex  33003  bj-exexbiex  33004  bj-biexal2  33010  bj-biexex  33013  bj-axrep1  33100  bj-axrep2  33101  bj-axrep3  33102  bj-axrep4  33103  bj-sbf3  33137  sbexi  34225  ac6s6  34288  e2ebind  39275  e2ebindVD  39640  e2ebindALT  39657  stoweidlem57  40751  ovncvrrp  41258
  Copyright terms: Public domain W3C validator