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

Theorem nfal 1511
Description: If 𝑥 is not free in 𝜑, it is not free in 𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfal.1 𝑥𝜑
Assertion
Ref Expression
nfal 𝑥𝑦𝜑

Proof of Theorem nfal
StepHypRef Expression
1 nfal.1 . . . 4 𝑥𝜑
21nfri 1455 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 1409 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nfi 1394 1 𝑥𝑦𝜑
Colors of variables: wff set class
Syntax hints:  wal 1285  wnf 1392
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-7 1380  ax-gen 1381  ax-4 1443
This theorem depends on definitions:  df-bi 115  df-nf 1393
This theorem is referenced by:  nfnf  1512  nfa2  1514  aaan  1522  cbv3  1674  cbv2  1679  nfald  1687  cbval2  1841  nfsb4t  1935  nfeuv  1963  mo23  1986  bm1.1  2070  nfnfc1  2228  nfnfc  2231  nfeq  2232  sbcnestgf  2968  dfnfc2  3654  nfdisjv  3813  nfdisj1  3814  nffr  4150  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  bdsepnft  11216  bdsepnfALT  11218  setindft  11298  strcollnft  11317  strcollnfALT  11319
  Copyright terms: Public domain W3C validator