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 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  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  4361  sbcnestgf  4366  nfdisjw  5064  nfdisj  5065  nfdisj1  5066  axrep1  5213  axrep2  5215  axrep3  5216  axrep4OLD  5219  nffr  5604  zfcndrep  10537  zfcndinf  10541  mreexexd  17614  mpteleeOLD  28964  mo5f  32558  iinabrex  32639  19.12b  35981  regsfromsetind  36721  bj-cbv2v  37105  ax11-pm2  37143  bj-axreprepsep  37382  wl-sb8t  37877  wl-mo2tf  37896  wl-eutf  37898  wl-mo2t  37900  wl-mo3t  37901  wl-sb8eut  37903  wl-sb8eutv  37904  mpobi123f  38483  pm11.57  44816  pm11.59  44818  permaxrep  45433  ichnfimlem  47923  ichnfim  47924  nfsetrecs  50161  pgind  50192