ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfal Structured version   GIF version

Theorem nfal 1450
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 1393 . . 3 (φxφ)
32hbal 1346 . 2 (yφxyφ)
43nfi 1331 1 xyφ
Colors of variables: wff set class
Syntax hints:  wal 1226  wnf 1329
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-7 1317  ax-gen 1318  ax-4 1381
This theorem depends on definitions:  df-bi 110  df-nf 1330
This theorem is referenced by:  nfnf  1451  nfa2  1453  aaan  1461  cbv3  1612  cbv2  1617  nfald  1625  cbval2  1778  nfsb4t  1872  nfeuv  1900  mo23  1923  bm1.1  2007  nfnfc1  2163  nfnfc  2166  nfeq  2167  sbcnestgf  2874  dfnfc2  3572  nfdisjv  3731  nfdisj1  3732  bdsepnft  7260  bdsepnfALT  7262  setindft  7330  strcollnft  7349  strcollnfALT  7351
  Copyright terms: Public domain W3C validator