Theorem nfal 2355

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 2233	. . 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 2215

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

This theorem is used by:  nfex  2356  nfnf  2358  cbval2v  2374  pm11.53  2377  19.12vv  2378  cbval2  2442  nfsb4t  2530  mof  2590  euf  2603  2eu3  2680  axextmo  2738  nfnfc1  2927  nfnfc  2936  sbcnestgfw  4382  sbcnestgf  4387  nfdisjw  5086  nfdisj  5087  nfdisj1  5088  axrep1  5237  axrep2  5239  axrep3  5240  axrep4OLD  5243  nffr  5632  zfcndrep  10627  zfcndinf  10631  mreexexd  17742  mpteleeOLD  29360  mo5f  32972  iinabrex  33050  axpowg3  35682  19.12b  36386  regsfromsetind  37166  bj-cbv2v  37549  ax11-pm2  37587  bj-axreprepsep  37828  wl-sb8t  38323  wl-mo2tf  38342  wl-eutf  38344  wl-mo2t  38346  wl-mo3t  38347  wl-sb8eut  38349  wl-sb8eutv  38350  mpobi123f  38918  pm11.57  45221  pm11.59  45223  permaxrep  45837  ichnfimlem  48371  ichnfim  48372  nfsetrecs  50620  pgind  50651  nfals  50740  nfalseu  50771