NFE Home 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-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-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