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

Theorem nfexd 1957
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 1618 . 2  |-  ( E. y ps  <->  -.  A. y  -.  ps )
2 nfald.1 . . . 4  |-  F/ y
ph
3 nfald.2 . . . . 5  |-  ( ph  ->  F/ x ps )
43nfnd 1907 . . . 4  |-  ( ph  ->  F/ x  -.  ps )
52, 4nfald 1956 . . 3  |-  ( ph  ->  F/ x A. y  -.  ps )
65nfnd 1907 . 2  |-  ( ph  ->  F/ x  -.  A. y  -.  ps )
71, 6nfxfrd 1651 1  |-  ( ph  ->  F/ x E. y ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1396   E.wex 1617   F/wnf 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622
This theorem is referenced by:  nfeud2  2298  nfeld  2624  axrepndlem1  8958  axrepndlem2  8959  axunndlem1  8961  axunnd  8962  axpowndlem2  8964  axpowndlem3  8965  axpowndlem4  8966  axregndlem2  8969  axinfndlem1  8972  axinfnd  8973  axacndlem4  8977  axacndlem5  8978  axacnd  8979  19.9d2rf  27578  hbexg  33742
  Copyright terms: Public domain W3C validator