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

Theorem nfnd 1760
Description: If  x is not free in  ph, it is not free in  -.  ph. (Contributed by Mario Carneiro, 24-Sep-2016.)
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 1757 . . 3  |-  F/ x F/ x ps
3 ax6o 1723 . . . . 5  |-  ( -. 
A. x  -.  A. x ps  ->  ps )
43con1i 121 . . . 4  |-  ( -. 
ps  ->  A. x  -.  A. x ps )
5 df-nf 1532 . . . . 5  |-  ( F/ x ps  <->  A. x
( ps  ->  A. x ps ) )
6 con3 126 . . . . . 6  |-  ( ( ps  ->  A. x ps )  ->  ( -. 
A. x ps  ->  -. 
ps ) )
76al2imi 1548 . . . . 5  |-  ( A. x ( ps  ->  A. x ps )  -> 
( A. x  -.  A. x ps  ->  A. x  -.  ps ) )
85, 7sylbi 187 . . . 4  |-  ( F/ x ps  ->  ( A. x  -.  A. x ps  ->  A. x  -.  ps ) )
94, 8syl5 28 . . 3  |-  ( F/ x ps  ->  ( -.  ps  ->  A. x  -.  ps ) )
102, 9nfd 1746 . 2  |-  ( F/ x ps  ->  F/ x  -.  ps )
111, 10syl 15 1  |-  ( ph  ->  F/ x  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1527   F/wnf 1531
This theorem is referenced by:  nfbid  1762  nfand  1763  nfn  1765  nfexd  1776  19.9t  1782  nfexd2  1913  cbvexd  1949  nfned  2541  nfneld  2542  nfrexd  2595  axpowndlem2  8220  axpowndlem3  8221  axpowndlem4  8222  axregndlem2  8225  axregnd  8226  distel  24160
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-nf 1532
  Copyright terms: Public domain W3C validator