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

Theorem nfe1 1706
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 1705 . 2  |-  ( E. x ph  ->  A. x E. x ph )
21nfi 1538 1  |-  F/ x E. x ph
Colors of variables: wff set class
Syntax hints:   E.wex 1528   F/wnf 1531
This theorem is referenced by:  excomim  1785  19.23t  1796  nf3  1799  19.38  1810  exan  1823  equs5e  1829  exdistrf  1911  nfmo1  2154  euan  2200  eupicka  2207  mopick2  2210  euor2  2211  moexex  2212  2moex  2214  2euex  2215  2moswap  2218  2eu4  2226  2eu7  2229  2eu8  2230  nfre1  2599  ceqsexg  2899  morex  2949  sbc6g  3016  intab  3892  nfopab1  4085  nfopab2  4086  axrep1  4132  axrep2  4133  axrep3  4134  axrep4  4135  copsexg  4252  copsex2t  4253  copsex2g  4254  mosubopt  4264  dfid3  4310  eusv2nf  4532  dmcoss  4944  imadif  5327  nfoprab1  5897  nfoprab2  5898  nfoprab3  5899  fsplit  6223  zfcndrep  8236  zfcndpow  8238  zfcndreg  8239  zfcndinf  8240  reclem2pr  8672  ex-natded9.26  20806  exisym1  24863  finminlem  26231  stoweidlem57  27806  e2ebind  28329  e2ebindVD  28688  e2ebindALT  28706  bnj607  28948  bnj849  28957  bnj1398  29064  bnj1449  29078
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-6 1703
This theorem depends on definitions:  df-bi 177  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator