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

Theorem nfex 1779
Description: If  x is not free in  ph, it is not free in  E. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nf.1  |-  F/ x ph
Assertion
Ref Expression
nfex  |-  F/ x E. y ph

Proof of Theorem nfex
StepHypRef Expression
1 df-ex 1532 . 2  |-  ( E. y ph  <->  -.  A. y  -.  ph )
2 nf.1 . . . . 5  |-  F/ x ph
32nfn 1777 . . . 4  |-  F/ x  -.  ph
43nfal 1778 . . 3  |-  F/ x A. y  -.  ph
54nfn 1777 . 2  |-  F/ x  -.  A. y  -.  ph
61, 5nfxfr 1560 1  |-  F/ x E. y ph
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1530   E.wex 1531   F/wnf 1534
This theorem is referenced by:  excomim  1797  eeor  1838  eean  1865  cbvex2  1958  nfeu1  2166  moexex  2225  nfel  2440  ceqsex2  2837  nfopab  4100  nfopab2  4102  cbvopab1  4105  cbvopab1s  4107  axrep2  4149  axrep3  4150  axrep4  4151  copsex2t  4269  copsex2g  4270  mosubopt  4280  euotd  4283  nfco  4865  dfdmf  4889  dfrnf  4933  nfdm  4936  fv3  5557  nfoprab2  5914  nfoprab3  5915  nfoprab  5916  cbvoprab1  5934  cbvoprab2  5935  cbvoprab3  5938  ac6sfi  7117  aceq1  7760  zfcndrep  8252  zfcndinf  8256  nfsum1  12179  nfsum  12180  fsum2dlem  12249  nfcprod1  24132  nfcprod  24133  nfprod1  25413  nfprod  25414  pm11.71  27699  stoweidlem57  27909  bnj981  29298  bnj1388  29379  bnj1445  29390  bnj1489  29402
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-tru 1310  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator