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

Theorem nfe1 1920
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 1919 . 2  |-  ( E. x ph  ->  A. x E. x ph )
21nfi 1676 1  |-  F/ x E. x ph
Colors of variables: wff setvar class
Syntax hints:   E.wex 1665   F/wnf 1669
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-10 1917
This theorem depends on definitions:  df-bi 189  df-ex 1666  df-nf 1670
This theorem is referenced by:  nf3  2044  exdistrf  2169  nfmo1  2312  euor2  2345  eupicka  2368  mopick2  2371  moexex  2372  2moex  2374  2euex  2375  2moswap  2378  2mo  2382  2eu7  2390  2eu8  2391  nfre1  2850  ceqsexg  3172  morex  3224  intab  4268  nfopab1  4472  nfopab2  4473  axrep1  4519  axrep2  4520  axrep3  4521  axrep4  4522  eusv2nf  4604  copsexg  4690  copsex2t  4691  copsex2g  4692  mosubopt  4702  dfid3  4753  dmcoss  5097  imadif  5663  nfoprab1  6345  nfoprab2  6346  nfoprab3  6347  fsplit  6906  zfcndrep  9044  zfcndpow  9046  zfcndreg  9047  zfcndinf  9048  reclem2pr  9478  ex-natded9.26  25881  brabgaf  28228  bnj607  29739  bnj849  29748  bnj1398  29855  bnj1449  29869  finminlem  30986  exisym1  31096  bj-alexbiex  31305  bj-exexbiex  31306  bj-biexal2  31312  bj-biexex  31315  bj-axrep1  31415  bj-axrep2  31416  bj-axrep3  31417  bj-axrep4  31418  bj-sbf3  31451  sbexi  32363  ac6s6  32427  e2ebind  36941  e2ebindVD  37319  e2ebindALT  37336  stoweidlem57  37928  ovncvrrp  38396
  Copyright terms: Public domain W3C validator