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

Theorem nfex 1767
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 1529 . 2  |-  ( E. y ph  <->  -.  A. y  -.  ph )
2 nf.1 . . . . 5  |-  F/ x ph
32nfn 1765 . . . 4  |-  F/ x  -.  ph
43nfal 1766 . . 3  |-  F/ x A. y  -.  ph
54nfn 1765 . 2  |-  F/ x  -.  A. y  -.  ph
61, 5nfxfr 1557 1  |-  F/ x E. y ph
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1527   E.wex 1528   F/wnf 1531
This theorem is referenced by:  excomim  1785  eeor  1826  eean  1853  cbvex2  1945  nfeu1  2153  moexex  2212  nfel  2427  ceqsex2  2824  nfopab  4084  nfopab2  4086  cbvopab1  4089  cbvopab1s  4091  axrep2  4133  axrep3  4134  axrep4  4135  copsex2t  4253  copsex2g  4254  mosubopt  4264  euotd  4267  nfco  4849  dfdmf  4873  dfrnf  4917  nfdm  4920  fv3  5541  nfoprab2  5898  nfoprab3  5899  nfoprab  5900  cbvoprab1  5918  cbvoprab2  5919  cbvoprab3  5922  ac6sfi  7101  aceq1  7744  zfcndrep  8236  zfcndinf  8240  nfsum1  12163  nfsum  12164  fsum2dlem  12233  nfprod1  25310  nfprod  25311  pm11.71  27596  stoweidlem57  27806  bnj981  28982  bnj1388  29063  bnj1445  29074  bnj1489  29086
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-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-tru 1310  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator