Theorem nfal 2355

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

Syntax hints:  ∀wal 1558  Ⅎwnf 1803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-10 2175  ax-11 2191  ax-12 2212

This theorem depends on definitions:  df-bi 209  df-ex 1800  df-nf 1804

This theorem is referenced by:  nfex  2356  nfnf  2358  cbval2v  2374  pm11.53  2377  19.12vv  2378  cbval2  2442  nfsb4t  2530  mof  2590  euf  2603  2eu3  2680  axextmo  2738  nfnfc1  2927  nfnfc  2936  sbcnestgfw  4375  sbcnestgf  4380  nfdisjw  5079  nfdisj  5080  nfdisj1  5081  axrep1  5228  axrep2  5230  axrep3  5231  axrep4OLD  5234  nffr  5620  zfcndrep  10572  zfcndinf  10576  mreexexd  17680  mpteleeOLD  29096  mo5f  32688  iinabrex  32769  axpowg3  35444  19.12b  36149  regsfromsetind  36899  bj-cbv2v  37283  ax11-pm2  37321  bj-axreprepsep  37560  wl-sb8t  38055  wl-mo2tf  38074  wl-eutf  38076  wl-mo2t  38078  wl-mo3t  38079  wl-sb8eut  38081  wl-sb8eutv  38082  mpobi123f  38661  pm11.57  44965  pm11.59  44967  permaxrep  45582  ichnfimlem  48069  ichnfim  48070  nfsetrecs  50307  pgind  50338