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  4384  sbcnestgf  4389  nfdisjw  5086  nfdisj  5087  nfdisj1  5088  axrep1  5235  axrep2  5237  axrep3  5238  axrep4OLD  5241  nffr  5611  zfcndrep  10567  zfcndinf  10571  mreexexd  17609  mptelee  28822  mo5f  32418  iinabrex  32498  19.12b  35789  bj-cbv2v  36786  ax11-pm2  36824  wl-sb8t  37540  wl-mo2tf  37559  wl-eutf  37561  wl-mo2t  37563  wl-mo3t  37564  wl-sb8eut  37566  wl-sb8eutv  37567  mpobi123f  38156  pm11.57  44378  pm11.59  44380  permaxrep  44996  ichnfimlem  47464  ichnfim  47465  nfsetrecs  49675  pgind  49706