Theorem nfal 2316

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

Syntax hints:  ∀wal 1539  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfex  2317  nfnf  2319  nfsbvOLD  2324  aaanOLD  2328  cbval2v  2339  pm11.53  2342  19.12vv  2343  cbval2  2410  nfsb4t  2498  mof  2557  euf  2570  2eu3  2649  axextmo  2707  nfnfc1  2906  nfnfc  2915  nfabdwOLD  2927  sbcnestgfw  4418  sbcnestgf  4423  nfdisjw  5125  nfdisj  5126  nfdisj1  5127  axrep1  5286  axrep2  5288  axrep3  5289  axrep4  5290  nffr  5650  zfcndrep  10608  zfcndinf  10612  mreexexd  17591  mptelee  28150  mo5f  31724  iinabrex  31795  19.12b  34768  bj-cbv2v  35671  ax11-pm2  35709  wl-sb8t  36412  wl-mo2tf  36431  wl-eutf  36433  wl-mo2t  36435  wl-mo3t  36436  wl-sb8eut  36437  mpobi123f  37025  pm11.57  43138  pm11.59  43140  ichnfimlem  46121  ichnfim  46122  nfsetrecs  47721  pgind  47752