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

Theorem nfe1 2155
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 2148 . 2 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
21nf5i 2151 1 𝑥𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wex 1781  wnf 1785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2146
This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786
This theorem is referenced by:  nfa1  2156  nfnf1  2159  nf6  2293  exdistrf  2471  nfeu1ALT  2676  euor2  2700  2moexv  2715  moexexvw  2716  2moswapv  2717  2euexv  2719  eupicka  2722  mopick2  2725  moexex  2726  2moex  2728  2euex  2729  2moswap  2732  2mo  2736  2eu7  2746  2eu8  2747  nfre1  3298  ceqsexg  3632  morex  3696  intab  4892  nfopab1  5121  nfopab2  5122  axrep1  5177  axrep2  5179  axrep3  5180  axrep4  5181  eusv2nf  5283  copsexgw  5368  copsexg  5369  copsex2t  5370  copsex2g  5371  mosubopt  5387  dfid3  5449  dmcoss  5829  imadif  6426  oprabidw  7180  nfoprab1  7208  nfoprab2  7209  nfoprab3  7210  fsplitOLD  7809  zfcndrep  10034  zfcndpow  10036  zfcndreg  10037  zfcndinf  10038  reclem2pr  10468  ex-natded9.26  28210  brabgaf  30373  bnj607  32248  bnj849  32257  bnj1398  32366  bnj1449  32380  finminlem  33726  exisym1  33832  bj-alexbiex  34093  bj-exexbiex  34094  bj-biexal2  34100  bj-biexex  34103  bj-sbf3  34224  copsex2d  34502  sbexi  35499  ac6s6  35558  e2ebind  41193  e2ebindVD  41542  e2ebindALT  41559  stoweidlem57  42629  ovncvrrp  43133  ich2ex  43915  ichreuopeq  43920  reuopreuprim  43973
  Copyright terms: Public domain W3C validator