Theorem nfal 2321

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

Syntax hints:  ∀wal 1537  Ⅎwnf 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2139  ax-11 2156  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788

This theorem is referenced by:  nfex  2322  nfnf  2324  nfsbvOLD  2329  aaan  2332  cbval2v  2342  cbval2vOLD  2343  pm11.53  2346  19.12vv  2347  cbval2  2411  nfsb4t  2503  mof  2563  euf  2576  2eu3  2655  axextmo  2713  nfnfc1  2909  nfnfc  2918  nfabdwOLD  2930  sbcnestgfw  4349  sbcnestgf  4354  nfdisjw  5047  nfdisj  5048  nfdisj1  5049  axrep1  5206  axrep2  5208  axrep3  5209  axrep4  5210  nffr  5554  zfcndrep  10301  zfcndinf  10305  mreexexd  17274  mptelee  27166  mo5f  30738  iinabrex  30809  19.12b  33683  bj-cbv2v  34907  ax11-pm2  34946  wl-sb8t  35634  wl-mo2tf  35653  wl-eutf  35655  wl-mo2t  35657  wl-mo3t  35658  wl-sb8eut  35659  mpobi123f  36247  pm11.57  41896  pm11.59  41898  ichnfimlem  44803  ichnfim  44804  nfsetrecs  46278