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

Theorem nfal 1484
 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 1428 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 1382 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nfi 1367 1 𝑥𝑦𝜑
 Colors of variables: wff set class Syntax hints:  ∀wal 1257  Ⅎwnf 1365 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-4 1416 This theorem depends on definitions:  df-bi 114  df-nf 1366 This theorem is referenced by:  nfnf  1485  nfa2  1487  aaan  1495  cbv3  1646  cbv2  1651  nfald  1659  cbval2  1812  nfsb4t  1906  nfeuv  1934  mo23  1957  bm1.1  2041  nfnfc1  2197  nfnfc  2200  nfeq  2201  sbcnestgf  2925  dfnfc2  3626  nfdisjv  3785  nfdisj1  3786  nffr  4114  bdsepnft  10394  bdsepnfALT  10396  setindft  10477  strcollnft  10496  strcollnfALT  10498
 Copyright terms: Public domain W3C validator