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

Theorem nfexd 2034
Description: If  x is not free in  ps, it is not free in  E. y ps. (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 1663 . 2  |-  ( E. y ps  <->  -.  A. y  -.  ps )
2 nfald.1 . . . 4  |-  F/ y
ph
3 nfald.2 . . . . 5  |-  ( ph  ->  F/ x ps )
43nfnd 1983 . . . 4  |-  ( ph  ->  F/ x  -.  ps )
52, 4nfald 2033 . . 3  |-  ( ph  ->  F/ x A. y  -.  ps )
65nfnd 1983 . 2  |-  ( ph  ->  F/ x  -.  A. y  -.  ps )
71, 6nfxfrd 1696 1  |-  ( ph  ->  F/ x E. y ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1441   E.wex 1662   F/wnf 1666
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1663  df-nf 1667
This theorem is referenced by:  nfeud2  2310  nfeld  2599  axrepndlem1  9014  axrepndlem2  9015  axunndlem1  9017  axunnd  9018  axpowndlem2  9020  axpowndlem3  9021  axpowndlem4  9022  axregndlem2  9025  axinfndlem1  9027  axinfnd  9028  axacndlem4  9032  axacndlem5  9033  axacnd  9034  19.9d2rf  28105  hbexg  36917
  Copyright terms: Public domain W3C validator