Theorem nfal 2328

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 2202	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	2	hbal 2172	. 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)
4	3	nf5i 2151	1 ⊢ Ⅎ𝑥∀𝑦𝜑

Syntax hints:  ∀wal 1539  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2146  ax-11 2162  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfex  2329  nfnf  2331  cbval2v  2347  pm11.53  2350  19.12vv  2351  cbval2  2415  nfsb4t  2503  mof  2563  euf  2576  2eu3  2654  axextmo  2712  nfnfc1  2901  nfnfc  2911  sbcnestgfw  4373  sbcnestgf  4378  nfdisjw  5077  nfdisj  5078  nfdisj1  5079  axrep1  5225  axrep2  5227  axrep3  5228  axrep4OLD  5231  nffr  5597  zfcndrep  10525  zfcndinf  10529  mreexexd  17571  mpteleeOLD  28968  mo5f  32563  iinabrex  32644  19.12b  35993  regsfromsetind  36669  bj-cbv2v  36999  ax11-pm2  37037  wl-sb8t  37757  wl-mo2tf  37776  wl-eutf  37778  wl-mo2t  37780  wl-mo3t  37781  wl-sb8eut  37783  wl-sb8eutv  37784  mpobi123f  38363  pm11.57  44640  pm11.59  44642  permaxrep  45257  ichnfimlem  47719  ichnfim  47720  nfsetrecs  49941  pgind  49972