Theorem nfal 2354

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

This proof depends on syntax axioms:  ∀wal 1568  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2178  ax-11 2194  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  nfex  2355  nfnf  2357  cbval2v  2373  pm11.53  2376  19.12vv  2377  cbval2  2441  nfsb4t  2529  mof  2589  euf  2602  2eu3  2679  axextmo  2737  nfnfc1  2926  nfnfc  2935  sbcnestgfw  4379  sbcnestgf  4384  nfdisjw  5082  nfdisj  5083  nfdisj1  5084  axrep1  5233  axrep2  5235  axrep3  5236  nffr  5624  zfcndrep  10699  zfcndinf  10703  mreexexd  17822  mpteleeOLD  29473  mo5f  33085  iinabrex  33163  axpowg3  35816  19.12b  36563  regsfromsetind  37327  bj-cbv2v  37710  ax11-pm2  37748  bj-axreprepsep  37991  wl-sb8t  38484  wl-mo2tf  38503  wl-eutf  38505  wl-mo2t  38507  wl-mo3t  38508  wl-sb8eut  38510  wl-sb8eutv  38511  mpobi123f  39094  pm11.57  45372  pm11.59  45374  permaxrep  45995  ichnfimlem  48544  ichnfim  48545  nfsetrecs  50788  pgind  50809  nfals  50898  nfalseu  50929