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

Theorem nfe1 1732
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 1731 . 2  |-  ( E. x ph  ->  A. x E. x ph )
21nfi 1551 1  |-  F/ x E. x ph
Colors of variables: wff set class
Syntax hints:   E.wex 1541   F/wnf 1544
This theorem is referenced by:  19.23tOLD  1821  excomimOLD  1863  nf3  1872  19.38OLD  1877  exanOLD  1886  equs5eOLD  1893  exdistrf  1976  nfmo1  2220  euan  2266  eupicka  2273  mopick2  2276  euor2  2277  moexex  2278  2moex  2280  2euex  2281  2moswap  2284  2eu4  2292  2eu7  2295  2eu8  2296  nfre1  2675  ceqsexg  2975  morex  3025  sbc6g  3092  intab  3971  nfopab1  4164  nfopab2  4165  axrep1  4211  axrep2  4212  axrep3  4213  axrep4  4214  copsexg  4331  copsex2t  4332  copsex2g  4333  mosubopt  4343  dfid3  4389  eusv2nf  4611  dmcoss  5023  imadif  5406  nfoprab1  5981  nfoprab2  5982  nfoprab3  5983  fsplit  6307  zfcndrep  8323  zfcndpow  8325  zfcndreg  8326  zfcndinf  8327  reclem2pr  8759  ex-natded9.26  20912  exisym1  25422  finminlem  25555  stoweidlem57  27129  e2ebind  28057  e2ebindVD  28433  e2ebindALT  28451  bnj607  28693  bnj849  28702  bnj1398  28809  bnj1449  28823  exdistrfNEW7  28911  excomimOLD7  29077
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-6 1729
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545
  Copyright terms: Public domain W3C validator