Theorem nfal 2362

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

Syntax hints:  ∀wal 1565  Ⅎwnf 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-10 2182  ax-11 2198  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811

This theorem is referenced by:  nfex  2363  nfnf  2365  cbval2v  2381  pm11.53  2384  19.12vv  2385  cbval2  2449  nfsb4t  2537  mof  2597  euf  2610  2eu3  2687  axextmo  2745  nfnfc1  2934  nfnfc  2943  sbcnestgfw  4392  sbcnestgf  4397  nfdisjw  5092  nfdisj  5093  nfdisj1  5094  axrep1  5243  axrep2  5245  axrep3  5246  axrep4OLD  5249  nffr  5635  zfcndrep  10599  zfcndinf  10603  mreexexd  17704  mpteleeOLD  29186  mo5f  32776  iinabrex  32855  axpowg3  35484  19.12b  36190  regsfromsetind  36939  bj-cbv2v  37322  ax11-pm2  37360  bj-axreprepsep  37600  wl-sb8t  38095  wl-mo2tf  38114  wl-eutf  38116  wl-mo2t  38118  wl-mo3t  38119  wl-sb8eut  38121  wl-sb8eutv  38122  mpobi123f  38701  pm11.57  44991  pm11.59  44993  permaxrep  45607  ichnfimlem  48101  ichnfim  48102  nfsetrecs  50349  pgind  50380  nfals  50466