Theorem nfal 2322

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

Syntax hints:  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfex  2323  nfnf  2325  cbval2v  2341  pm11.53  2344  19.12vv  2345  cbval2  2409  nfsb4t  2497  mof  2556  euf  2569  2eu3  2647  axextmo  2705  nfnfc1  2894  nfnfc  2904  sbcnestgfw  4372  sbcnestgf  4377  nfdisjw  5071  nfdisj  5072  nfdisj1  5073  axrep1  5219  axrep2  5221  axrep3  5222  axrep4OLD  5225  nffr  5592  zfcndrep  10508  zfcndinf  10512  mreexexd  17554  mptelee  28840  mo5f  32433  iinabrex  32513  19.12b  35779  bj-cbv2v  36776  ax11-pm2  36814  wl-sb8t  37530  wl-mo2tf  37549  wl-eutf  37551  wl-mo2t  37553  wl-mo3t  37554  wl-sb8eut  37556  wl-sb8eutv  37557  mpobi123f  38146  pm11.57  44366  pm11.59  44368  permaxrep  44984  ichnfimlem  47451  ichnfim  47452  nfsetrecs  49675  pgind  49706