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

Theorem nfe1 2176
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 2170 . 2 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
21nf5i 2173 1 𝑥𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wex 1853  wnf 1857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-10 2168
This theorem depends on definitions:  df-bi 197  df-ex 1854  df-nf 1859
This theorem is referenced by:  nfa1  2177  nfnf1  2180  nf6  2264  exdistrf  2473  nfmo1  2618  euor2  2652  eupicka  2675  mopick2  2678  moexex  2679  2moex  2681  2euex  2682  2moswap  2685  2mo  2689  2eu7  2697  2eu8  2698  nfre1  3143  ceqsexg  3473  morex  3531  intab  4659  nfopab1  4871  nfopab2  4872  axrep1  4924  axrep2  4925  axrep3  4926  axrep4  4927  eusv2nf  5013  copsexg  5104  copsex2t  5105  copsex2g  5106  mosubopt  5120  dfid3  5175  dmcoss  5540  imadif  6134  nfoprab1  6870  nfoprab2  6871  nfoprab3  6872  fsplit  7451  zfcndrep  9648  zfcndpow  9650  zfcndreg  9651  zfcndinf  9652  reclem2pr  10082  ex-natded9.26  27608  brabgaf  29748  bnj607  31314  bnj849  31323  bnj1398  31430  bnj1449  31444  finminlem  32639  exisym1  32750  bj-alexbiex  33018  bj-exexbiex  33019  bj-biexal2  33025  bj-biexex  33028  bj-axrep1  33116  bj-axrep2  33117  bj-axrep3  33118  bj-axrep4  33119  bj-sbf3  33154  sbexi  34247  ac6s6  34311  e2ebind  39299  e2ebindVD  39665  e2ebindALT  39682  stoweidlem57  40795  ovncvrrp  41302
  Copyright terms: Public domain W3C validator