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

Theorem nfe1 1747
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 1746 . 2  |-  ( E. x ph  ->  A. x E. x ph )
21nfi 1560 1  |-  F/ x E. x ph
Colors of variables: wff set class
Syntax hints:   E.wex 1550   F/wnf 1553
This theorem is referenced by:  19.23tOLD  1838  excomimOLD  1881  nf3  1890  19.38OLD  1895  exanOLD  1904  equs5eOLD  1911  exdistrf  2062  exdistrfOLD  2063  nfmo1  2291  euan  2337  eupicka  2344  mopick2  2347  euor2  2348  moexex  2349  2moex  2351  2euex  2352  2moswap  2355  2eu4  2363  2eu7  2366  2eu8  2367  nfre1  2754  ceqsexg  3059  morex  3110  sbc6g  3178  intab  4072  nfopab1  4266  nfopab2  4267  axrep1  4313  axrep2  4314  axrep3  4315  axrep4  4316  copsexg  4434  copsex2t  4435  copsex2g  4436  mosubopt  4446  dfid3  4491  eusv2nf  4713  dmcoss  5127  imadif  5520  nfoprab1  6115  nfoprab2  6116  nfoprab3  6117  fsplit  6443  zfcndrep  8481  zfcndpow  8483  zfcndreg  8484  zfcndinf  8485  reclem2pr  8917  ex-natded9.26  21719  exisym1  26166  finminlem  26312  stoweidlem57  27773  e2ebind  28587  e2ebindVD  28961  e2ebindALT  28978  bnj607  29224  bnj849  29233  bnj1398  29340  bnj1449  29354  exdistrfNEW7  29442  excomimOLD7  29630
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-6 1744
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator