Theorem nfal 2353

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 2231	. . 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  2354  nfnf  2356  cbval2v  2372  pm11.53  2375  19.12vv  2376  cbval2  2440  nfsb4t  2528  mof  2588  euf  2601  2eu3  2678  axextmo  2736  nfnfc1  2925  nfnfc  2934  sbcnestgfw  4379  sbcnestgf  4384  nfdisjw  5082  nfdisj  5083  nfdisj1  5084  axrep1  5233  axrep2  5235  axrep3  5236  axrep4OLD  5239  nffr  5628  zfcndrep  10624  zfcndinf  10628  mreexexd  17737  mpteleeOLD  29353  mo5f  32965  iinabrex  33043  axpowg3  35675  19.12b  36379  regsfromsetind  37159  bj-cbv2v  37542  ax11-pm2  37580  bj-axreprepsep  37821  wl-sb8t  38316  wl-mo2tf  38335  wl-eutf  38337  wl-mo2t  38339  wl-mo3t  38340  wl-sb8eut  38342  wl-sb8eutv  38343  mpobi123f  38911  pm11.57  45214  pm11.59  45216  permaxrep  45830  ichnfimlem  48364  ichnfim  48365  nfsetrecs  50613  pgind  50644  nfals  50733  nfalseu  50764