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  2410  nfsb4t  2498  mof  2557  euf  2570  2eu3  2648  axextmo  2706  nfnfc1  2895  nfnfc  2905  sbcnestgfw  4387  sbcnestgf  4392  nfdisjw  5089  nfdisj  5090  nfdisj1  5091  axrep1  5238  axrep2  5240  axrep3  5241  axrep4OLD  5244  nffr  5614  zfcndrep  10574  zfcndinf  10578  mreexexd  17616  mptelee  28829  mo5f  32425  iinabrex  32505  19.12b  35796  bj-cbv2v  36793  ax11-pm2  36831  wl-sb8t  37547  wl-mo2tf  37566  wl-eutf  37568  wl-mo2t  37570  wl-mo3t  37571  wl-sb8eut  37573  wl-sb8eutv  37574  mpobi123f  38163  pm11.57  44385  pm11.59  44387  permaxrep  45003  ichnfimlem  47468  ichnfim  47469  nfsetrecs  49679  pgind  49710