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

Theorem nfe1 1739
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 1738 . 2  |-  ( E. x ph  ->  A. x E. x ph )
21nfi 1557 1  |-  F/ x E. x ph
Colors of variables: wff set class
Syntax hints:   E.wex 1547   F/wnf 1550
This theorem is referenced by:  19.23tOLD  1828  excomimOLD  1870  nf3  1879  19.38OLD  1884  exanOLD  1893  equs5eOLD  1900  exdistrf  2010  nfmo1  2249  euan  2295  eupicka  2302  mopick2  2305  euor2  2306  moexex  2307  2moex  2309  2euex  2310  2moswap  2313  2eu4  2321  2eu7  2324  2eu8  2325  nfre1  2705  ceqsexg  3010  morex  3061  sbc6g  3129  intab  4022  nfopab1  4215  nfopab2  4216  axrep1  4262  axrep2  4263  axrep3  4264  axrep4  4265  copsexg  4383  copsex2t  4384  copsex2g  4385  mosubopt  4395  dfid3  4440  eusv2nf  4661  dmcoss  5075  imadif  5468  nfoprab1  6062  nfoprab2  6063  nfoprab3  6064  fsplit  6390  zfcndrep  8422  zfcndpow  8424  zfcndreg  8425  zfcndinf  8426  reclem2pr  8858  ex-natded9.26  21575  exisym1  25888  finminlem  26012  stoweidlem57  27474  e2ebind  27993  e2ebindVD  28365  e2ebindALT  28383  bnj607  28625  bnj849  28634  bnj1398  28741  bnj1449  28755  exdistrfNEW7  28843  excomimOLD7  29009
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-6 1736
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator