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

Theorem nfe1 2150
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 2143 . 2 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
21nf5i 2146 1 𝑥𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wex 1779  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2141
This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784
This theorem is referenced by:  nfa1  2151  nfnf1  2154  sbalex  2242  nf6  2283  exdistrf  2452  nfeu1ALT  2589  euor2  2613  2moexv  2627  moexexvw  2628  2moswapv  2629  2euexv  2631  eupicka  2634  mopick2  2637  moexex  2638  2moex  2640  2euex  2641  2moswap  2644  2mo  2648  2eu7  2658  2eu8  2659  nfre1  3285  ceqsexg  3653  morex  3725  intab  4978  nfopab1  5213  nfopab2  5214  axrep1  5280  axrep2  5282  axrep3  5283  axrep4OLD  5286  eusv2nf  5395  copsexgw  5495  copsexg  5496  copsex2t  5497  mosubopt  5515  dfid3  5581  dmcoss  5985  imadif  6650  oprabidw  7462  nfoprab1  7494  nfoprab2  7495  nfoprab3  7496  zfcndrep  10654  zfcndpow  10656  zfcndreg  10657  zfcndinf  10658  reclem2pr  11088  ex-natded9.26  30438  brabgaf  32620  bnj607  34930  bnj849  34939  bnj1398  35048  bnj1449  35062  finminlem  36319  exisym1  36425  bj-alexbiex  36700  bj-exexbiex  36701  bj-biexal2  36707  bj-biexex  36710  bj-sbf3  36840  copsex2d  37140  sbexi  38120  ac6s6  38179  e2ebind  44583  e2ebindVD  44932  e2ebindALT  44949  stoweidlem57  46072  ovncvrrp  46579  ich2ex  47455  ichreuopeq  47460  reuopreuprim  47513  pgind  49236
  Copyright terms: Public domain W3C validator