Theorem nfal 1590

Description: If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1524. (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 1475	. . . . . 6 ⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
2	1	biimpi 120	. . . . 5 ⊢ (Ⅎ𝑥𝜑 → ∀𝑥(𝜑 → ∀𝑥𝜑))
3	2	alimi 1469	. . . 4 ⊢ (∀𝑦Ⅎ𝑥𝜑 → ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
4		ax-7 1462	. . . 4 ⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑))
5		ax-5 1461	. . . . . 6 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑))
6		ax-7 1462	. . . . . 6 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)
7	5, 6	syl6 33	. . . . 5 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))
8	7	alimi 1469	. . . 4 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))
9	3, 4, 8	3syl 17	. . 3 ⊢ (∀𝑦Ⅎ𝑥𝜑 → ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))
10		df-nf 1475	. . 3 ⊢ (Ⅎ𝑥∀𝑦𝜑 ↔ ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))
11	9, 10	sylibr 134	. 2 ⊢ (∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥∀𝑦𝜑)
12		nfal.1	. 2 ⊢ Ⅎ𝑥𝜑
13	11, 12	mpg 1465	1 ⊢ Ⅎ𝑥∀𝑦𝜑

Syntax hints:   → wi 4  ∀wal 1362  Ⅎwnf 1474

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 1461  ax-7 1462  ax-gen 1463

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

This theorem is referenced by:  nfnf  1591  nfa2  1593  aaan  1601  cbv3  1756  cbv2  1763  nfald  1774  cbval2  1936  nfsb4t  2033  nfeuv  2063  mo23  2086  bm1.1  2181  nfnfc1  2342  nfnfc  2346  nfeq  2347  nfabdw  2358  sbcnestgf  3136  dfnfc2  3857  nfdisjv  4022  nfdisj1  4023  nffr  4384  uchoice  6195  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidunben  12643  bdsepnft  15533  bdsepnfALT  15535  setindft  15611  strcollnft  15630  pw1nct  15647