Theorem nfal 2324

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 2198	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	2	hbal 2170	. 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)
4	3	nf5i 2149	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 2144  ax-11 2160  ax-12 2180

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

This theorem is referenced by:  nfex  2325  nfnf  2327  cbval2v  2343  pm11.53  2346  19.12vv  2347  cbval2  2411  nfsb4t  2499  mof  2558  euf  2571  2eu3  2649  axextmo  2707  nfnfc1  2897  nfnfc  2907  sbcnestgfw  4368  sbcnestgf  4373  nfdisjw  5068  nfdisj  5069  nfdisj1  5070  axrep1  5216  axrep2  5218  axrep3  5219  axrep4OLD  5222  nffr  5587  zfcndrep  10505  zfcndinf  10509  mreexexd  17554  mptelee  28873  mo5f  32468  iinabrex  32549  19.12b  35843  bj-cbv2v  36842  ax11-pm2  36880  wl-sb8t  37596  wl-mo2tf  37615  wl-eutf  37617  wl-mo2t  37619  wl-mo3t  37620  wl-sb8eut  37622  wl-sb8eutv  37623  mpobi123f  38212  pm11.57  44492  pm11.59  44494  permaxrep  45109  ichnfimlem  47573  ichnfim  47574  nfsetrecs  49797  pgind  49828