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

Theorem nfexd 1879
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 1588 . 2  |-  ( E. y ps  <->  -.  A. y  -.  ps )
2 nfald.1 . . . 4  |-  F/ y
ph
3 nfald.2 . . . . 5  |-  ( ph  ->  F/ x ps )
43nfnd 1837 . . . 4  |-  ( ph  ->  F/ x  -.  ps )
52, 4nfald 1878 . . 3  |-  ( ph  ->  F/ x A. y  -.  ps )
65nfnd 1837 . 2  |-  ( ph  ->  F/ x  -.  A. y  -.  ps )
71, 6nfxfrd 1617 1  |-  ( ph  ->  F/ x E. y ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1368   E.wex 1587   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591
This theorem is referenced by:  nfeud2  2274  nfeld  2618  axrepndlem1  8843  axrepndlem2  8844  axunndlem1  8846  axunnd  8847  axpowndlem2  8849  axpowndlem2OLD  8850  axpowndlem3  8851  axpowndlem3OLD  8852  axpowndlem4  8853  axregndlem2  8856  axinfndlem1  8859  axinfnd  8860  axacndlem4  8864  axacndlem5  8865  axacnd  8866  19.9d2rf  25983  hbexg  31547
  Copyright terms: Public domain W3C validator