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

Theorem nfn 1777
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 1772 . 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 1534
This theorem is referenced by:  nfex  1779  nfor  1782  nfan  1783  19.32  1823  nfnae  1909  equsex  1915  spime  1929  cbvex  1938  ax15  1974  sb8e  2046  mo  2178  euor  2183  euor2  2224  2mo  2234  nfne  2552  nfnel  2553  nfrex  2611  cbvrexf  2772  spcimegf  2875  spcegf  2877  cbvrexcsf  3157  nfdif  3310  nfpo  4335  nffr  4383  rexxpf  4847  boxcutc  6875  nfoi  7245  itgaddnclem2  25010  stoweidlem34  27886  stoweidlem55  27907  stoweidlem59  27911  r19.32  28048  0neqopab  28192  a9e2ndeqALT  29024  bnj1476  29195  bnj1388  29379  bnj1398  29380  bnj1445  29390  bnj1449  29394  nfexwAUX7  29428  nfnaewAUX7  29459  nfnaew2AUX7  29462  nfeqfNEW7  29463  equsexNEW7  29467  exdistrfNEW7  29482  spimeNEW7  29486  cbvexwAUX7  29495  nfnaew3AUX7  29501  ax15NEW7  29511  nfsb2NEW7  29536  sbco2wAUX7  29559  sbco3wAUX7  29561  sbcomwAUX7  29562  sb8ewAUX7  29566  nfexOLD7  29642  nfnaeOLD7  29665  cbvexOLD7  29680  dvelimfOLD7  29681  nfsb4tw2AUXOLD7  29700  dvelimdfOLD7  29705  sbco2OLD7  29706  sbcomOLD7  29709  sb8eOLD7  29711  sb9iOLD7  29712  a12study  29754  a12study2  29756  cdlemefs32sn1aw  31225
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-tru 1310  df-nf 1535
  Copyright terms: Public domain W3C validator