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

Theorem nfn 1765
Description: If  x is not free in  ph, it is not free in  -.  ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nf.1  |-  F/ x ph
Assertion
Ref Expression
nfn  |-  F/ x  -.  ph

Proof of Theorem nfn
StepHypRef Expression
1 nf.1 . . . 4  |-  F/ x ph
21a1i 10 . . 3  |-  (  T. 
->  F/ x ph )
32nfnd 1760 . 2  |-  (  T. 
->  F/ x  -.  ph )
43trud 1314 1  |-  F/ x  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    T. wtru 1307   F/wnf 1531
This theorem is referenced by:  nfex  1767  nfor  1770  nfan  1771  19.32  1811  nfnae  1896  equsex  1902  spime  1916  cbvex  1925  ax15  1961  sb8e  2033  mo  2165  euor  2170  euor2  2211  2mo  2221  nfne  2539  nfnel  2540  nfrex  2598  cbvrexf  2759  spcimegf  2862  spcegf  2864  cbvrexcsf  3144  nfdif  3297  nfpo  4319  nffr  4367  rexxpf  4831  boxcutc  6859  nfoi  7229  stoweidlem34  27783  stoweidlem55  27804  stoweidlem59  27808  r19.32  27945  a9e2ndeqALT  28708  bnj1476  28879  bnj1388  29063  bnj1398  29064  bnj1445  29074  bnj1449  29078  a12study  29132  a12study2  29134  cdlemefs32sn1aw  30603
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-tru 1310  df-nf 1532
  Copyright terms: Public domain W3C validator