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

Theorem nfe1 1743
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 1742 . 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  1834  excomimOLD  1877  nf3  1886  19.38OLD  1891  exanOLD  1900  equs5eOLD  1907  exdistrf  2028  nfmo1  2265  euan  2311  eupicka  2318  mopick2  2321  euor2  2322  moexex  2323  2moex  2325  2euex  2326  2moswap  2329  2eu4  2337  2eu7  2340  2eu8  2341  nfre1  2722  ceqsexg  3027  morex  3078  sbc6g  3146  intab  4040  nfopab1  4234  nfopab2  4235  axrep1  4281  axrep2  4282  axrep3  4283  axrep4  4284  copsexg  4402  copsex2t  4403  copsex2g  4404  mosubopt  4414  dfid3  4459  eusv2nf  4680  dmcoss  5094  imadif  5487  nfoprab1  6082  nfoprab2  6083  nfoprab3  6084  fsplit  6410  zfcndrep  8445  zfcndpow  8447  zfcndreg  8448  zfcndinf  8449  reclem2pr  8881  ex-natded9.26  21680  exisym1  26078  finminlem  26211  stoweidlem57  27673  e2ebind  28361  e2ebindVD  28733  e2ebindALT  28751  bnj607  28993  bnj849  29002  bnj1398  29109  bnj1449  29123  exdistrfNEW7  29211  excomimOLD7  29377
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 1740
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator