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

Theorem nfexd 1899
Description: If  x is not free in  ph, it is not free in  E. y ph. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
nfald.1  |-  F/ y
ph
nfald.2  |-  ( ph  ->  F/ x ps )
Assertion
Ref Expression
nfexd  |-  ( ph  ->  F/ x E. y ps )

Proof of Theorem nfexd
StepHypRef Expression
1 df-ex 1597 . 2  |-  ( E. y ps  <->  -.  A. y  -.  ps )
2 nfald.1 . . . 4  |-  F/ y
ph
3 nfald.2 . . . . 5  |-  ( ph  ->  F/ x ps )
43nfnd 1850 . . . 4  |-  ( ph  ->  F/ x  -.  ps )
52, 4nfald 1898 . . 3  |-  ( ph  ->  F/ x A. y  -.  ps )
65nfnd 1850 . 2  |-  ( ph  ->  F/ x  -.  A. y  -.  ps )
71, 6nfxfrd 1626 1  |-  ( ph  ->  F/ x E. y ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1377   E.wex 1596   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600
This theorem is referenced by:  nfeud2  2290  nfeld  2637  axrepndlem1  8963  axrepndlem2  8964  axunndlem1  8966  axunnd  8967  axpowndlem2  8969  axpowndlem2OLD  8970  axpowndlem3  8971  axpowndlem3OLD  8972  axpowndlem4  8973  axregndlem2  8976  axinfndlem1  8979  axinfnd  8980  axacndlem4  8984  axacndlem5  8985  axacnd  8986  19.9d2rf  27053  hbexg  32409
  Copyright terms: Public domain W3C validator