Theorem nfal 2322

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

Syntax hints:  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfex  2323  nfnf  2325  cbval2v  2341  pm11.53  2344  19.12vv  2345  cbval2  2409  nfsb4t  2497  mof  2556  euf  2569  2eu3  2647  axextmo  2705  nfnfc1  2894  nfnfc  2904  sbcnestgfw  4380  sbcnestgf  4385  nfdisjw  5081  nfdisj  5082  nfdisj1  5083  axrep1  5230  axrep2  5232  axrep3  5233  axrep4OLD  5236  nffr  5604  zfcndrep  10543  zfcndinf  10547  mreexexd  17585  mptelee  28798  mo5f  32391  iinabrex  32471  19.12b  35762  bj-cbv2v  36759  ax11-pm2  36797  wl-sb8t  37513  wl-mo2tf  37532  wl-eutf  37534  wl-mo2t  37536  wl-mo3t  37537  wl-sb8eut  37539  wl-sb8eutv  37540  mpobi123f  38129  pm11.57  44351  pm11.59  44353  permaxrep  44969  ichnfimlem  47437  ichnfim  47438  nfsetrecs  49648  pgind  49679