Theorem nfal 2358

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 2234	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	2	hbal 2205	. 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)
4	3	nf5i 2184	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 2179  ax-11 2195  ax-12 2216

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

This theorem is used by:  nfex  2359  nfnf  2361  cbval2v  2377  pm11.53  2380  19.12vv  2381  cbval2  2445  nfsb4t  2533  mof  2593  euf  2606  2eu3  2683  axextmo  2741  nfnfc1  2930  nfnfc  2939  sbcnestgfw  4386  sbcnestgf  4391  nfdisjw  5090  nfdisj  5091  nfdisj1  5092  axrep1  5241  axrep2  5243  axrep3  5244  axrep4OLD  5247  nffr  5636  zfcndrep  10616  zfcndinf  10620  mreexexd  17728  mpteleeOLD  29302  mo5f  32908  iinabrex  32987  axpowg3  35620  19.12b  36330  regsfromsetind  37109  bj-cbv2v  37492  ax11-pm2  37530  bj-axreprepsep  37771  wl-sb8t  38266  wl-mo2tf  38285  wl-eutf  38287  wl-mo2t  38289  wl-mo3t  38290  wl-sb8eut  38292  wl-sb8eutv  38293  mpobi123f  38871  pm11.57  45159  pm11.59  45161  permaxrep  45775  ichnfimlem  48272  ichnfim  48273  nfsetrecs  50523  pgind  50554  nfals  50640  nfalseu  50671