Theorem nfal 1555

Description: If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfal.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfal	⊢ Ⅎ𝑥∀𝑦𝜑

Proof of Theorem nfal

Step	Hyp	Ref	Expression
1		nfal.1	. . . 4 ⊢ Ⅎ𝑥𝜑
2	1	nfri 1499	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	2	hbal 1453	. 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)
4	3	nfi 1438	1 ⊢ Ⅎ𝑥∀𝑦𝜑

Syntax hints:  ∀wal 1329  Ⅎwnf 1436

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 1423  ax-7 1424  ax-gen 1425  ax-4 1487

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

This theorem is referenced by:  nfnf  1556  nfa2  1558  aaan  1566  cbv3  1720  cbv2  1725  nfald  1733  cbval2  1891  nfsb4t  1987  nfeuv  2015  mo23  2038  bm1.1  2122  nfnfc1  2282  nfnfc  2286  nfeq  2287  sbcnestgf  3046  dfnfc2  3749  nfdisjv  3913  nfdisj1  3914  nffr  4266  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  exmidunben  11928  bdsepnft  13074  bdsepnfALT  13076  setindft  13152  strcollnft  13171  strcollnfALT  13173