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

Theorem nfexd 1869
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 1548 . 2  |-  ( E. y ps  <->  -.  A. y  -.  ps )
2 nfald.1 . . . 4  |-  F/ y
ph
3 nfald.2 . . . . 5  |-  ( ph  ->  F/ x ps )
43nfnd 1805 . . . 4  |-  ( ph  ->  F/ x  -.  ps )
52, 4nfald 1867 . . 3  |-  ( ph  ->  F/ x A. y  -.  ps )
65nfnd 1805 . 2  |-  ( ph  ->  F/ x  -.  A. y  -.  ps )
71, 6nfxfrd 1577 1  |-  ( ph  ->  F/ x E. y ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1546   E.wex 1547   F/wnf 1550
This theorem is referenced by:  nfeld  2563  axrepndlem1  8431  axrepndlem2  8432  axunndlem1  8434  axunnd  8435  axpowndlem2  8437  axpowndlem3  8438  axpowndlem4  8439  axregndlem2  8442  axinfndlem1  8444  axinfnd  8445  axacndlem4  8449  axacndlem5  8450  axacnd  8451  19.9d2rf  23929  hbexg  28362
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator