Theorem nfal 2329

Description: If 𝑥 is not free in 𝜑, then 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	nf5ri 2203	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	2	hbal 2173	. 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)
4	3	nf5i 2152	1 ⊢ Ⅎ𝑥∀𝑦𝜑

Syntax hints:  ∀wal 1540  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfex  2330  nfnf  2332  cbval2v  2348  pm11.53  2351  19.12vv  2352  cbval2  2416  nfsb4t  2504  mof  2564  euf  2577  2eu3  2655  axextmo  2713  nfnfc1  2902  nfnfc  2912  sbcnestgfw  4362  sbcnestgf  4367  nfdisjw  5065  nfdisj  5066  nfdisj1  5067  axrep1  5214  axrep2  5216  axrep3  5217  axrep4OLD  5220  nffr  5598  zfcndrep  10531  zfcndinf  10535  mreexexd  17608  mpteleeOLD  28981  mo5f  32576  iinabrex  32657  19.12b  36000  regsfromsetind  36740  bj-cbv2v  37124  ax11-pm2  37162  bj-axreprepsep  37401  wl-sb8t  37894  wl-mo2tf  37913  wl-eutf  37915  wl-mo2t  37917  wl-mo3t  37918  wl-sb8eut  37920  wl-sb8eutv  37921  mpobi123f  38500  pm11.57  44837  pm11.59  44839  permaxrep  45454  ichnfimlem  47938  ichnfim  47939  nfsetrecs  50176  pgind  50207