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

Theorem nfal 1586
Description: If 𝑥 is not free in 𝜑, it is not free in 𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1520. (Revised by Gino Giotto, 25-Aug-2024.)
Hypothesis
Ref Expression
nfal.1 𝑥𝜑
Assertion
Ref Expression
nfal 𝑥𝑦𝜑

Proof of Theorem nfal
StepHypRef Expression
1 df-nf 1471 . . . . . 6 (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
21biimpi 120 . . . . 5 (Ⅎ𝑥𝜑 → ∀𝑥(𝜑 → ∀𝑥𝜑))
32alimi 1465 . . . 4 (∀𝑦𝑥𝜑 → ∀𝑦𝑥(𝜑 → ∀𝑥𝜑))
4 ax-7 1458 . . . 4 (∀𝑦𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥𝑦(𝜑 → ∀𝑥𝜑))
5 ax-5 1457 . . . . . 6 (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑦𝑥𝜑))
6 ax-7 1458 . . . . . 6 (∀𝑦𝑥𝜑 → ∀𝑥𝑦𝜑)
75, 6syl6 33 . . . . 5 (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑥𝑦𝜑))
87alimi 1465 . . . 4 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥(∀𝑦𝜑 → ∀𝑥𝑦𝜑))
93, 4, 83syl 17 . . 3 (∀𝑦𝑥𝜑 → ∀𝑥(∀𝑦𝜑 → ∀𝑥𝑦𝜑))
10 df-nf 1471 . . 3 (Ⅎ𝑥𝑦𝜑 ↔ ∀𝑥(∀𝑦𝜑 → ∀𝑥𝑦𝜑))
119, 10sylibr 134 . 2 (∀𝑦𝑥𝜑 → Ⅎ𝑥𝑦𝜑)
12 nfal.1 . 2 𝑥𝜑
1311, 12mpg 1461 1 𝑥𝑦𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1361  wnf 1470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-7 1458  ax-gen 1459
This theorem depends on definitions:  df-bi 117  df-nf 1471
This theorem is referenced by:  nfnf  1587  nfa2  1589  aaan  1597  cbv3  1752  cbv2  1759  nfald  1770  cbval2  1931  nfsb4t  2024  nfeuv  2054  mo23  2077  bm1.1  2172  nfnfc1  2332  nfnfc  2336  nfeq  2337  nfabdw  2348  sbcnestgf  3120  dfnfc2  3839  nfdisjv  4004  nfdisj1  4005  nffr  4361  exmidfodomrlemr  7214  exmidfodomrlemrALT  7215  exmidunben  12440  bdsepnft  14910  bdsepnfALT  14912  setindft  14988  strcollnft  15007  pw1nct  15024
  Copyright terms: Public domain W3C validator