Theorem nfal 2326

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 2200	. . 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 2182

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

This theorem is referenced by:  nfex  2327  nfnf  2329  cbval2v  2345  pm11.53  2348  19.12vv  2349  cbval2  2413  nfsb4t  2501  mof  2561  euf  2574  2eu3  2652  axextmo  2710  nfnfc1  2899  nfnfc  2909  sbcnestgfw  4371  sbcnestgf  4376  nfdisjw  5075  nfdisj  5076  nfdisj1  5077  axrep1  5223  axrep2  5225  axrep3  5226  axrep4OLD  5229  nffr  5595  zfcndrep  10523  zfcndinf  10527  mreexexd  17569  mpteleeOLD  28917  mo5f  32512  iinabrex  32593  19.12b  35942  bj-cbv2v  36942  ax11-pm2  36980  wl-sb8t  37696  wl-mo2tf  37715  wl-eutf  37717  wl-mo2t  37719  wl-mo3t  37720  wl-sb8eut  37722  wl-sb8eutv  37723  mpobi123f  38302  pm11.57  44572  pm11.59  44574  permaxrep  45189  ichnfimlem  47651  ichnfim  47652  nfsetrecs  49873  pgind  49904