Theorem nfal 1625

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

Syntax hints:   → wi 4  ∀wal 1396  Ⅎwnf 1509

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 1496  ax-7 1497  ax-gen 1498

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

This theorem is referenced by:  nfnf  1626  nfa2  1628  aaan  1636  cbv3  1791  cbv2  1798  nfald  1809  cbval2  1971  nfsb4t  2068  nfeuv  2098  mo23  2122  bm1.1  2217  nfnfc1  2387  nfnfc  2391  nfeq  2392  nfabdw  2403  sbcnestgf  3190  dfnfc2  3932  nfdisjv  4097  nfdisj1  4098  nffr  4470  uchoice  6331  modom  7061  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  exmidunben  13177  bdsepnft  16657  bdsepnfALT  16659  setindft  16735  strcollnft  16754  pw1nct  16777