Theorem nfal 2322

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

Syntax hints:  ∀wal 1541  Ⅎwnf 1791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-10 2141  ax-11 2158  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-ex 1788  df-nf 1792

This theorem is referenced by:  nfex  2323  nfnf  2325  nfsbvOLD  2330  aaan  2333  cbval2v  2343  cbval2vOLD  2344  pm11.53  2347  19.12vv  2348  cbval2  2410  nfsb4t  2502  mof  2562  euf  2575  2eu3  2654  axextmo  2712  nfnfc1  2907  nfnfc  2916  nfabdwOLD  2928  sbcnestgfw  4333  sbcnestgf  4338  nfdisjw  5030  nfdisj  5031  nfdisj1  5032  axrep1  5180  axrep2  5182  axrep3  5183  axrep4  5184  nffr  5525  zfcndrep  10228  zfcndinf  10232  mreexexd  17151  mptelee  26986  mo5f  30556  iinabrex  30627  19.12b  33496  bj-cbv2v  34717  ax11-pm2  34756  wl-sb8t  35444  wl-mo2tf  35463  wl-eutf  35465  wl-mo2t  35467  wl-mo3t  35468  wl-sb8eut  35469  mpobi123f  36057  pm11.57  41680  pm11.59  41682  ichnfimlem  44588  ichnfim  44589  nfsetrecs  46063