Theorem nfal 2151

Description: If 𝑥 is not free in 𝜑, 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 2063	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
3	2	hbal 2034	. 2 ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑)
4	3	nf5i 2022	1 ⊢ Ⅎ𝑥∀𝑦𝜑

Syntax hints:  ∀wal 1479  Ⅎwnf 1706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-10 2017  ax-11 2032  ax-12 2045

This theorem depends on definitions:  df-bi 197  df-ex 1703  df-nf 1708

This theorem is referenced by:  nfex  2152  nfnf  2156  nfaldOLD  2164  nfa2OLD  2166  aaan  2168  cbv3v  2170  pm11.53  2177  19.12vv  2178  cbv3  2263  cbval2  2277  nfsb4t  2387  euf  2476  mo2  2477  2eu3  2553  bm1.1  2605  nfnfc1  2765  nfnfc  2771  nfnfcALT  2772  sbcnestgf  3986  dfnfc2OLD  4446  nfdisj  4623  nfdisj1  4624  axrep1  4763  axrep2  4764  axrep3  4765  axrep4  4766  nffr  5078  zfcndrep  9421  zfcndinf  9425  mreexexd  16289  mreexexdOLD  16290  mptelee  25756  mo5f  29296  19.12b  31681  bj-cbv2v  32707  bj-cbval2v  32712  bj-axrep1  32763  bj-axrep2  32764  bj-axrep3  32765  bj-axrep4  32766  ax11-pm2  32798  bj-nfnfc  32828  wl-sb8t  33304  wl-mo2tf  33324  wl-eutf  33326  wl-mo2t  33328  wl-mo3t  33329  wl-sb8eut  33330  mpt2bi123f  33942  pm11.57  38409  pm11.59  38411  nfsetrecs  42198