Theorem nfal 2332

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

Syntax hints:  ∀wal 1545  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-10 2152  ax-11 2168  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfex  2333  nfnf  2335  cbval2v  2351  pm11.53  2354  19.12vv  2355  cbval2  2419  nfsb4t  2507  mof  2567  euf  2580  2eu3  2657  axextmo  2715  nfnfc1  2904  nfnfc  2913  sbcnestgfw  4349  sbcnestgf  4354  nfdisjw  5051  nfdisj  5052  nfdisj1  5053  axrep1  5200  axrep2  5202  axrep3  5203  axrep4OLD  5206  nffr  5591  zfcndrep  10528  zfcndinf  10532  mreexexd  17605  mpteleeOLD  28982  mo5f  32576  iinabrex  32658  axpowg3  35329  19.12b  36027  regsfromsetind  36767  bj-cbv2v  37151  ax11-pm2  37189  bj-axreprepsep  37428  wl-sb8t  37923  wl-mo2tf  37942  wl-eutf  37944  wl-mo2t  37946  wl-mo3t  37947  wl-sb8eut  37949  wl-sb8eutv  37950  mpobi123f  38529  pm11.57  44833  pm11.59  44835  permaxrep  45450  ichnfimlem  47938  ichnfim  47939  nfsetrecs  50176  pgind  50207