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

Theorem nfe1 1718
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 1717 . 2  |-  ( E. x ph  ->  A. x E. x ph )
21nfi 1541 1  |-  F/ x E. x ph
Colors of variables: wff set class
Syntax hints:   E.wex 1531   F/wnf 1534
This theorem is referenced by:  excomim  1797  19.23t  1808  nf3  1811  19.38  1822  exan  1835  equs5e  1841  exdistrf  1924  nfmo1  2167  euan  2213  eupicka  2220  mopick2  2223  euor2  2224  moexex  2225  2moex  2227  2euex  2228  2moswap  2231  2eu4  2239  2eu7  2242  2eu8  2243  nfre1  2612  ceqsexg  2912  morex  2962  sbc6g  3029  intab  3908  nfopab1  4101  nfopab2  4102  axrep1  4148  axrep2  4149  axrep3  4150  axrep4  4151  copsexg  4268  copsex2t  4269  copsex2g  4270  mosubopt  4280  dfid3  4326  eusv2nf  4548  dmcoss  4960  imadif  5343  nfoprab1  5913  nfoprab2  5914  nfoprab3  5915  fsplit  6239  zfcndrep  8252  zfcndpow  8254  zfcndreg  8255  zfcndinf  8256  reclem2pr  8688  ex-natded9.26  20822  exisym1  24935  finminlem  26334  stoweidlem57  27909  e2ebind  28628  e2ebindVD  29004  e2ebindALT  29022  bnj607  29264  bnj849  29273  bnj1398  29380  bnj1449  29394  exdistrfNEW7  29482  excomimOLD7  29647
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-6 1715
This theorem depends on definitions:  df-bi 177  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator