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

Theorem nfnd 1792
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 1791 . . 3  |-  F/ x F/ x ps
3 df-nf 1545 . . . 4  |-  ( F/ x ps  <->  A. x
( ps  ->  A. x ps ) )
4 hbnt 1776 . . . 4  |-  ( A. x ( ps  ->  A. x ps )  -> 
( -.  ps  ->  A. x  -.  ps )
)
53, 4sylbi 187 . . 3  |-  ( F/ x ps  ->  ( -.  ps  ->  A. x  -.  ps ) )
62, 5nfd 1767 . 2  |-  ( F/ x ps  ->  F/ x  -.  ps )
71, 6syl 15 1  |-  ( ph  ->  F/ x  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1540   F/wnf 1544
This theorem is referenced by:  nfn  1794  nfand  1826  nfbidOLD  1838  nfexd  1859  19.9tOLD  1862  nfexd2  1978  cbvexd  2014  nfned  2617  nfneld  2618  nfrexd  2671  axpowndlem2  8310  axpowndlem3  8311  axpowndlem4  8312  axregndlem2  8315  axregnd  8316  distel  24718  nfexdwAUX7  28876  nfexdOLD7  29092  nfexd2OLD7  29119  cbvexdOLD7  29136
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545
  Copyright terms: Public domain W3C validator