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

Theorem nfnd 1805
Description: If in a context  x is not free in  ps, it is not free in  -.  ps. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.)
Hypothesis
Ref Expression
nfnd.1  |-  ( ph  ->  F/ x ps )
Assertion
Ref Expression
nfnd  |-  ( ph  ->  F/ x  -.  ps )

Proof of Theorem nfnd
StepHypRef Expression
1 nfnd.1 . 2  |-  ( ph  ->  F/ x ps )
2 nfnf1 1804 . . 3  |-  F/ x F/ x ps
3 df-nf 1551 . . . 4  |-  ( F/ x ps  <->  A. x
( ps  ->  A. x ps ) )
4 hbnt 1795 . . . 4  |-  ( A. x ( ps  ->  A. x ps )  -> 
( -.  ps  ->  A. x  -.  ps )
)
53, 4sylbi 188 . . 3  |-  ( F/ x ps  ->  ( -.  ps  ->  A. x  -.  ps ) )
62, 5nfd 1778 . 2  |-  ( F/ x ps  ->  F/ x  -.  ps )
71, 6syl 16 1  |-  ( ph  ->  F/ x  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1546   F/wnf 1550
This theorem is referenced by:  nfn  1807  nfand  1839  nfbidOLD  1851  nfexd  1869  19.9tOLD  1876  nfexd2  2030  cbvexd  2059  nfned  2659  nfneld  2664  nfrexd  2718  axpowndlem2  8429  axpowndlem3  8430  axpowndlem4  8431  axregndlem2  8434  axregnd  8435  distel  25374  nfexdwAUX7  29159  nfexdOLD7  29375  nfexd2OLD7  29402  cbvexdOLD7  29419
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-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator