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

Theorem nfe1 1840
Description: is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfe1

Proof of Theorem nfe1
StepHypRef Expression
1 hbe1 1839 . 2
21nfi 1623 1
Colors of variables: wff setvar class
Syntax hints:  E.wex 1612  F/wnf 1616
This theorem is referenced by:  nf3  1961  exdistrf  2075  nfmo1  2295  euor2  2333  eupicka  2359  mopick2  2362  moexex  2363  2moex  2365  2euex  2366  2moswap  2369  2mo  2373  2moOLD  2374  2eu4OLD  2381  2eu7  2385  2eu8  2386  nfre1  2918  ceqsexg  3231  morex  3283  intab  4317  nfopab1  4518  nfopab2  4519  axrep1  4564  axrep2  4565  axrep3  4566  axrep4  4567  eusv2nf  4650  copsexg  4737  copsexgOLD  4738  copsex2t  4739  copsex2g  4740  mosubopt  4750  dfid3  4801  dmcoss  5267  imadif  5668  nfoprab1  6346  nfoprab2  6347  nfoprab3  6348  fsplit  6905  zfcndrep  9013  zfcndpow  9015  zfcndreg  9016  zfcndinf  9017  reclem2pr  9447  ex-natded9.26  25140  exisym1  29889  finminlem  30136  sbexi  30516  ac6s6  30580  stoweidlem57  31839  e2ebind  33336  e2ebindVD  33712  e2ebindALT  33729  bnj607  33974  bnj849  33983  bnj1398  34090  bnj1449  34104  bj-alexbiex  34253  bj-exexbiex  34254  bj-biexal2  34260  bj-biexex  34263  bj-axrep1  34374  bj-axrep2  34375  bj-axrep3  34376  bj-axrep4  34377  bj-sbf3  34410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-10 1837
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator