Theorem nfal 1622

Description: If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1556. (Revised by GG, 25-Aug-2024.)

Hypothesis

Ref	Expression
nfal.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfal	⊢ Ⅎ𝑥∀𝑦𝜑

Proof of Theorem nfal

Step	Hyp	Ref	Expression
1		df-nf 1507	. . . . . 6 ⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
2	1	biimpi 120	. . . . 5 ⊢ (Ⅎ𝑥𝜑 → ∀𝑥(𝜑 → ∀𝑥𝜑))
3	2	alimi 1501	. . . 4 ⊢ (∀𝑦Ⅎ𝑥𝜑 → ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
4		ax-7 1494	. . . 4 ⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑))
5		ax-5 1493	. . . . . 6 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑))
6		ax-7 1494	. . . . . 6 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)
7	5, 6	syl6 33	. . . . 5 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))
8	7	alimi 1501	. . . 4 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))
9	3, 4, 8	3syl 17	. . 3 ⊢ (∀𝑦Ⅎ𝑥𝜑 → ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))
10		df-nf 1507	. . 3 ⊢ (Ⅎ𝑥∀𝑦𝜑 ↔ ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))
11	9, 10	sylibr 134	. 2 ⊢ (∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥∀𝑦𝜑)
12		nfal.1	. 2 ⊢ Ⅎ𝑥𝜑
13	11, 12	mpg 1497	1 ⊢ Ⅎ𝑥∀𝑦𝜑

Syntax hints:   → wi 4  ∀wal 1393  Ⅎwnf 1506

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 1493  ax-7 1494  ax-gen 1495

This theorem depends on definitions:  df-bi 117  df-nf 1507

This theorem is referenced by:  nfnf  1623  nfa2  1625  aaan  1633  cbv3  1788  cbv2  1795  nfald  1806  cbval2  1968  nfsb4t  2065  nfeuv  2095  mo23  2119  bm1.1  2214  nfnfc1  2375  nfnfc  2379  nfeq  2380  nfabdw  2391  sbcnestgf  3176  dfnfc2  3906  nfdisjv  4071  nfdisj1  4072  nffr  4440  uchoice  6289  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidunben  13012  bdsepnft  16305  bdsepnfALT  16307  setindft  16383  strcollnft  16402  pw1nct  16428