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

Theorem nfe1 1789
Description:  x is not free in  E. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfe1  |-  F/ x E. x ph

Proof of Theorem nfe1
StepHypRef Expression
1 hbe1 1788 . 2  |-  ( E. x ph  ->  A. x E. x ph )
21nfi 1606 1  |-  F/ x E. x ph
Colors of variables: wff setvar class
Syntax hints:   E.wex 1596   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-10 1786
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600
This theorem is referenced by:  nf3  1910  exdistrf  2048  nfmo1  2289  euor2  2334  euor2OLD  2335  euanOLD  2354  eupicka  2365  mopick2  2370  moexex  2371  moexexOLD  2372  2moex  2374  2euex  2375  2moswap  2378  2mo  2382  2moOLD  2383  2eu4OLD  2391  2eu7  2395  2eu8  2396  nfre1  2925  ceqsexg  3235  morex  3287  sbc6g  3357  intab  4312  nfopab1  4513  nfopab2  4514  axrep1  4559  axrep2  4560  axrep3  4561  axrep4  4562  eusv2nf  4645  copsexg  4732  copsexgOLD  4733  copsex2t  4734  copsex2g  4735  mosubopt  4745  dfid3  4796  dmcoss  5262  imadif  5663  nfoprab1  6330  nfoprab2  6331  nfoprab3  6332  fsplit  6888  zfcndrep  8992  zfcndpow  8994  zfcndreg  8995  zfcndinf  8996  reclem2pr  9426  ex-natded9.26  24845  exisym1  29494  finminlem  29741  sbexi  30147  sbcexf  30149  ac6s6  30212  stoweidlem57  31385  e2ebind  32434  e2ebindVD  32810  e2ebindALT  32827  bnj607  33071  bnj849  33080  bnj1398  33187  bnj1449  33201  bj-alexbiex  33353  bj-exexbiex  33354  bj-biexal2  33360  bj-biexex  33363  bj-axrep1  33473  bj-axrep2  33474  bj-axrep3  33475  bj-axrep4  33476  bj-sbf3  33509
  Copyright terms: Public domain W3C validator