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  17589  mptelee  28875  mo5f  32468  iinabrex  32548  19.12b  35782  bj-cbv2v  36779  ax11-pm2  36817  wl-sb8t  37533  wl-mo2tf  37552  wl-eutf  37554  wl-mo2t  37556  wl-mo3t  37557  wl-sb8eut  37559  wl-sb8eutv  37560  mpobi123f  38149  pm11.57  44371  pm11.59  44373  permaxrep  44989  ichnfimlem  47457  ichnfim  47458  nfsetrecs  49668  pgind  49699