Theorem nfal 2321

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

Syntax hints:  ∀wal 1534  Ⅎwnf 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-10 2138  ax-11 2154  ax-12 2174

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

This theorem is referenced by:  nfex  2322  nfnf  2324  nfsbvOLD  2329  aaanOLD  2332  cbval2v  2343  pm11.53  2346  19.12vv  2347  cbval2  2413  nfsb4t  2501  mof  2560  euf  2573  2eu3  2651  axextmo  2709  nfnfc1  2905  nfnfc  2915  sbcnestgfw  4426  sbcnestgf  4431  nfdisjw  5126  nfdisj  5127  nfdisj1  5128  axrep1  5285  axrep2  5287  axrep3  5288  axrep4OLD  5291  nffr  5661  zfcndrep  10651  zfcndinf  10655  mreexexd  17692  mptelee  28924  mo5f  32516  iinabrex  32588  19.12b  35782  bj-cbv2v  36780  ax11-pm2  36818  wl-sb8t  37532  wl-mo2tf  37551  wl-eutf  37553  wl-mo2t  37555  wl-mo3t  37556  wl-sb8eut  37558  wl-sb8eutv  37559  mpobi123f  38148  pm11.57  44384  pm11.59  44386  ichnfimlem  47387  ichnfim  47388  nfsetrecs  48916  pgind  48947