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

Theorem nfal 1842
 Description: If x is not free in φ, it is not free in ∀yφ. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfal.1 xφ
Assertion
Ref Expression
nfal xyφ

Proof of Theorem nfal
StepHypRef Expression
1 nfal.1 . . . 4 xφ
21nfri 1762 . . 3 (φxφ)
32hbal 1736 . 2 (yφxyφ)
43nfi 1551 1 xyφ
 Colors of variables: wff setvar class Syntax hints:  ∀wal 1540  Ⅎwnf 1544 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-7 1734  ax-11 1746 This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545 This theorem is referenced by:  nfexOLD  1844  nfnf  1845  nfnfOLD  1846  nfald  1852  nfaldOLD  1853  nfa2  1855  aaan  1884  pm11.53  1893  19.12vv  1898  cbval2  2004  sb8  2092  euf  2210  mo  2226  2mo  2282  2eu3  2286  bm1.1  2338  nfnfc1  2492  nfnfc  2495  nfeq  2496  sbcnestgf  3183  dfnfc2  3909
 Copyright terms: Public domain W3C validator