Theorem nfal 2323

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 2195	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	2	hbal 2167	. 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)
4	3	nf5i 2146	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 2007  ax-10 2141  ax-11 2157  ax-12 2177

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

This theorem is referenced by:  nfex  2324  nfnf  2326  aaanOLD  2333  cbval2v  2344  pm11.53  2347  19.12vv  2348  cbval2  2415  nfsb4t  2503  mof  2562  euf  2575  2eu3  2653  axextmo  2711  nfnfc1  2901  nfnfc  2911  sbcnestgfw  4396  sbcnestgf  4401  nfdisjw  5098  nfdisj  5099  nfdisj1  5100  axrep1  5250  axrep2  5252  axrep3  5253  axrep4OLD  5256  nffr  5627  zfcndrep  10628  zfcndinf  10632  mreexexd  17660  mptelee  28874  mo5f  32470  iinabrex  32550  19.12b  35819  bj-cbv2v  36816  ax11-pm2  36854  wl-sb8t  37570  wl-mo2tf  37589  wl-eutf  37591  wl-mo2t  37593  wl-mo3t  37594  wl-sb8eut  37596  wl-sb8eutv  37597  mpobi123f  38186  pm11.57  44413  pm11.59  44415  permaxrep  45031  ichnfimlem  47477  ichnfim  47478  nfsetrecs  49550  pgind  49581