New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfn GIF version

Theorem nfn 1793
 Description: If x is not free in φ, it is not free in ¬ φ. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfn.1 xφ
Assertion
Ref Expression
nfn x ¬ φ

Proof of Theorem nfn
StepHypRef Expression
1 nfn.1 . . . 4 xφ
21a1i 10 . . 3 ( ⊤ → Ⅎxφ)
32nfnd 1791 . 2 ( ⊤ → Ⅎx ¬ φ)
43trud 1323 1 x ¬ φ
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ⊤ wtru 1316  Ⅎwnf 1544 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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-tru 1319  df-ex 1542  df-nf 1545 This theorem is referenced by:  nfnan  1825  nfanOLD  1826  nfor  1836  nfexOLD  1844  19.32  1875  nfnae  1956  equsex  1962  spime  1976  cbvex  1985  ax15  2021  sb8e  2093  mo  2226  euor  2231  euor2  2272  2mo  2282  nfne  2610  nfnel  2611  nfrex  2669  cbvrexf  2830  spcimegf  2933  spcegf  2935  cbvrexcsf  3199  rexxpf  4828
 Copyright terms: Public domain W3C validator