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

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

Proof of Theorem nfn
StepHypRef Expression
1 nfn.1 . . . 4  |-  F/ x ph
21a1i 11 . . 3  |-  (  T. 
->  F/ x ph )
32nfnd 1799 . 2  |-  (  T. 
->  F/ x  -.  ph )
43trud 1329 1  |-  F/ x  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    T. wtru 1322   F/wnf 1550
This theorem is referenced by:  nfnan  1837  nfanOLD  1838  nfor  1848  nfexOLD  1856  19.32  1885  spimeOLD  1951  equsexOLD  1960  nfnae  2002  cbvex  2022  ax15  2055  mo  2261  euor  2266  euor2  2307  2mo  2317  nfne  2642  nfnel  2647  nfrex  2705  cbvrexf  2871  spcimegf  2974  spcegf  2976  cbvrexcsf  3256  nfdif  3412  nfpo  4450  nffr  4498  rexxpf  4961  0neqopab  6059  boxcutc  7042  nfoi  7417  itgaddnclem2  25965  stoweidlem34  27452  stoweidlem55  27473  stoweidlem59  27477  r19.32  27614  a9e2ndeqALT  28386  bnj1476  28557  bnj1388  28741  bnj1398  28742  bnj1445  28752  bnj1449  28756  nfexwAUX7  28790  nfnaewAUX7  28821  nfnaew2AUX7  28824  nfeqfNEW7  28825  equsexNEW7  28829  exdistrfNEW7  28844  spimeNEW7  28848  cbvexwAUX7  28857  nfnaew3AUX7  28863  ax15NEW7  28873  nfsb2NEW7  28898  sbco2wAUX7  28921  sb8ewAUX7  28928  nfexOLD7  29005  nfnaeOLD7  29028  cbvexOLD7  29043  dvelimfOLD7  29044  nfsb4tw2AUXOLD7  29063  dvelimdfOLD7  29068  sbco2OLD7  29069  sbcomOLD7  29072  sb8eOLD7  29074  sb9iOLD7  29075  cdlemefs32sn1aw  30529
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 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-tru 1325  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator