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

Theorem nfe1 1748
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 1747 . 2  |-  ( E. x ph  ->  A. x E. x ph )
21nfi 1561 1  |-  F/ x E. x ph
Colors of variables: wff set class
Syntax hints:   E.wex 1551   F/wnf 1554
This theorem is referenced by:  19.23tOLD  1839  excomimOLD  1882  nf3  1891  19.38OLD  1896  exanOLD  1905  equs5eOLD  1912  exdistrf  2067  exdistrfOLD  2068  nfmo1  2294  euan  2340  eupicka  2347  mopick2  2350  euor2  2351  moexex  2352  2moex  2354  2euex  2355  2moswap  2358  2eu4  2366  2eu7  2369  2eu8  2370  nfre1  2764  ceqsexg  3069  morex  3120  sbc6g  3188  intab  4082  nfopab1  4276  nfopab2  4277  axrep1  4323  axrep2  4324  axrep3  4325  axrep4  4326  copsexg  4444  copsex2t  4445  copsex2g  4446  mosubopt  4456  dfid3  4501  eusv2nf  4723  dmcoss  5137  imadif  5530  nfoprab1  6125  nfoprab2  6126  nfoprab3  6127  fsplit  6453  zfcndrep  8491  zfcndpow  8493  zfcndreg  8494  zfcndinf  8495  reclem2pr  8927  ex-natded9.26  21729  exisym1  26176  finminlem  26323  stoweidlem57  27784  e2ebind  28712  e2ebindVD  29086  e2ebindALT  29103  bnj607  29349  bnj849  29358  bnj1398  29465  bnj1449  29479  exdistrfNEW7  29567  excomimOLD7  29755
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-6 1745
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator