Theorem nfal 2139

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

Syntax hints:  ∀wal 1473  Ⅎwnf 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701

This theorem is referenced by:  nfex  2140  nfnf  2144  nfaldOLD  2152  nfa2OLD  2154  aaan  2156  cbv3v  2158  pm11.53  2167  19.12vv  2168  cbv3  2253  cbvalv  2261  cbval2  2267  nfsb4t  2377  euf  2466  mo2  2467  2eu3  2543  bm1.1  2595  nfnfc1  2754  nfnfc  2760  nfnfcALT  2761  sbcnestgf  3947  dfnfc2OLD  4391  nfdisj  4565  nfdisj1  4566  axrep1  4700  axrep2  4701  axrep3  4702  axrep4  4703  nffr  5012  zfcndrep  9315  zfcndinf  9319  mreexexd  16131  mreexexdOLD  16132  mptelee  25575  mo5f  28708  19.12b  30951  bj-cbv2v  31919  bj-cbval2v  31924  bj-axrep1  31976  bj-axrep2  31977  bj-axrep3  31978  bj-axrep4  31979  ax11-pm2  32011  bj-nfnfc  32047  wl-sb8t  32512  wl-mo2tf  32532  wl-eutf  32534  wl-mo2t  32536  wl-mo3t  32537  wl-sb8eut  32538  mpt2bi123f  33141  pm11.57  37611  pm11.59  37613  nfsetrecs  42232