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

Theorem nfe1 2145
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 2138 . 2 (∃𝑥𝜑 → ∀𝑥𝑥𝜑)
21nf5i 2141 1 𝑥𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wex 1771  wnf 1775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-10 2136
This theorem depends on definitions:  df-bi 208  df-ex 1772  df-nf 1776
This theorem is referenced by:  nfa1  2146  nfnf1  2149  nf6  2282  exdistrf  2461  nfeu1ALT  2668  euor2  2690  2moexv  2705  moexexvw  2706  2moswapv  2707  2euexv  2709  eupicka  2712  mopick2  2715  moexex  2716  2moex  2718  2euex  2719  2moswap  2722  2mo  2726  2eu7  2738  2eu8  2739  nfre1  3303  ceqsexg  3643  morex  3707  intab  4897  nfopab1  5126  nfopab2  5127  axrep1  5182  axrep2  5184  axrep3  5185  axrep4  5186  eusv2nf  5286  copsexgw  5372  copsexg  5373  copsex2t  5374  copsex2g  5375  mosubopt  5391  dfid3  5455  dmcoss  5835  imadif  6431  oprabidw  7176  nfoprab1  7204  nfoprab2  7205  nfoprab3  7206  fsplitOLD  7802  zfcndrep  10024  zfcndpow  10026  zfcndreg  10027  zfcndinf  10028  reclem2pr  10458  ex-natded9.26  28125  brabgaf  30287  bnj607  32087  bnj849  32096  bnj1398  32203  bnj1449  32217  finminlem  33563  exisym1  33669  bj-alexbiex  33930  bj-exexbiex  33931  bj-biexal2  33937  bj-biexex  33940  bj-sbf3  34059  copsex2d  34323  sbexi  35272  ac6s6  35331  e2ebind  40774  e2ebindVD  41123  e2ebindALT  41140  stoweidlem57  42219  ovncvrrp  42723  ich2ex  43506  ichreuopeq  43512  reuopreuprim  43565
  Copyright terms: Public domain W3C validator