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  nfsbvOLD  2331  aaanOLD  2334  cbval2v  2345  pm11.53  2348  19.12vv  2349  cbval2  2416  nfsb4t  2504  mof  2563  euf  2576  2eu3  2654  axextmo  2712  nfnfc1  2908  nfnfc  2918  sbcnestgfw  4421  sbcnestgf  4426  nfdisjw  5122  nfdisj  5123  nfdisj1  5124  axrep1  5280  axrep2  5282  axrep3  5283  axrep4OLD  5286  nffr  5658  zfcndrep  10654  zfcndinf  10658  mreexexd  17691  mptelee  28910  mo5f  32508  iinabrex  32582  19.12b  35802  bj-cbv2v  36799  ax11-pm2  36837  wl-sb8t  37553  wl-mo2tf  37572  wl-eutf  37574  wl-mo2t  37576  wl-mo3t  37577  wl-sb8eut  37579  wl-sb8eutv  37580  mpobi123f  38169  pm11.57  44408  pm11.59  44410  ichnfimlem  47450  ichnfim  47451  nfsetrecs  49205  pgind  49236