Theorem nfal 1624

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

Syntax hints:   → wi 4  ∀wal 1395  Ⅎwnf 1508

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

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

This theorem is referenced by:  nfnf  1625  nfa2  1627  aaan  1635  cbv3  1790  cbv2  1797  nfald  1808  cbval2  1970  nfsb4t  2067  nfeuv  2097  mo23  2121  bm1.1  2216  nfnfc1  2377  nfnfc  2381  nfeq  2382  nfabdw  2393  sbcnestgf  3179  dfnfc2  3911  nfdisjv  4076  nfdisj1  4077  nffr  4446  uchoice  6300  modom  6994  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidunben  13052  bdsepnft  16508  bdsepnfALT  16510  setindft  16586  strcollnft  16605  pw1nct  16630