Theorem nfal 1569

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

Hypothesis

Ref	Expression
nfal.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfal	⊢ Ⅎ𝑥∀𝑦𝜑

Proof of Theorem nfal

Step	Hyp	Ref	Expression
1		df-nf 1454	. . . . . 6 ⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
2	1	biimpi 119	. . . . 5 ⊢ (Ⅎ𝑥𝜑 → ∀𝑥(𝜑 → ∀𝑥𝜑))
3	2	alimi 1448	. . . 4 ⊢ (∀𝑦Ⅎ𝑥𝜑 → ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
4		ax-7 1441	. . . 4 ⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑))
5		ax-5 1440	. . . . . 6 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑦∀𝑥𝜑))
6		ax-7 1441	. . . . . 6 ⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)
7	5, 6	syl6 33	. . . . 5 ⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))
8	7	alimi 1448	. . . 4 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))
9	3, 4, 8	3syl 17	. . 3 ⊢ (∀𝑦Ⅎ𝑥𝜑 → ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))
10		df-nf 1454	. . 3 ⊢ (Ⅎ𝑥∀𝑦𝜑 ↔ ∀𝑥(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))
11	9, 10	sylibr 133	. 2 ⊢ (∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥∀𝑦𝜑)
12		nfal.1	. 2 ⊢ Ⅎ𝑥𝜑
13	11, 12	mpg 1444	1 ⊢ Ⅎ𝑥∀𝑦𝜑

Syntax hints:   → wi 4  ∀wal 1346  Ⅎwnf 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442

This theorem depends on definitions:  df-bi 116  df-nf 1454

This theorem is referenced by:  nfnf  1570  nfa2  1572  aaan  1580  cbv3  1735  cbv2  1742  nfald  1753  cbval2  1914  nfsb4t  2007  nfeuv  2037  mo23  2060  bm1.1  2155  nfnfc1  2315  nfnfc  2319  nfeq  2320  nfabdw  2331  sbcnestgf  3100  dfnfc2  3814  nfdisjv  3978  nfdisj1  3979  nffr  4334  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidunben  12381  bdsepnft  13922  bdsepnfALT  13924  setindft  14000  strcollnft  14019  pw1nct  14036