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

Theorem nfe1 2024
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 2018 . 2 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
21nf5i 2021 1 𝑥𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wex 1701  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-10 2016
This theorem depends on definitions:  df-bi 197  df-ex 1702  df-nf 1707
This theorem is referenced by:  nfa1  2025  nfnf1  2028  nf6  2114  exdistrf  2332  nfmo1  2480  euor2  2513  eupicka  2536  mopick2  2539  moexex  2540  2moex  2542  2euex  2543  2moswap  2546  2mo  2550  2eu7  2558  2eu8  2559  nfre1  3001  ceqsexg  3322  morex  3377  intab  4479  nfopab1  4691  nfopab2  4692  axrep1  4742  axrep2  4743  axrep3  4744  axrep4  4745  eusv2nf  4834  copsexg  4926  copsex2t  4927  copsex2g  4928  mosubopt  4942  dfid3  5000  dmcoss  5355  imadif  5941  nfoprab1  6669  nfoprab2  6670  nfoprab3  6671  abnex  6929  fsplit  7242  zfcndrep  9396  zfcndpow  9398  zfcndreg  9399  zfcndinf  9400  reclem2pr  9830  ex-natded9.26  27164  brabgaf  29304  bnj607  30747  bnj849  30756  bnj1398  30863  bnj1449  30877  finminlem  32007  exisym1  32118  bj-alexbiex  32385  bj-exexbiex  32386  bj-biexal2  32392  bj-biexex  32395  bj-axrep1  32484  bj-axrep2  32485  bj-axrep3  32486  bj-axrep4  32487  bj-sbf3  32522  sbexi  33587  ac6s6  33651  e2ebind  38300  e2ebindVD  38670  e2ebindALT  38687  stoweidlem57  39611  ovncvrrp  40115
  Copyright terms: Public domain W3C validator