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  4375  sbcnestgf  4380  nfdisjw  5079  nfdisj  5080  nfdisj1  5081  axrep1  5227  axrep2  5229  axrep3  5230  axrep4OLD  5233  nffr  5605  zfcndrep  10537  zfcndinf  10541  mreexexd  17583  mpteleeOLD  28980  mo5f  32575  iinabrex  32656  19.12b  36015  regsfromsetind  36691  bj-cbv2v  37046  ax11-pm2  37084  bj-axreprepsep  37323  wl-sb8t  37807  wl-mo2tf  37826  wl-eutf  37828  wl-mo2t  37830  wl-mo3t  37831  wl-sb8eut  37833  wl-sb8eutv  37834  mpobi123f  38413  pm11.57  44745  pm11.59  44747  permaxrep  45362  ichnfimlem  47823  ichnfim  47824  nfsetrecs  50045  pgind  50076