Theorem nfal 2317

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

Syntax hints:  ∀wal 1537  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfex  2318  nfnf  2320  nfsbvOLD  2325  aaanOLD  2329  cbval2v  2340  cbval2vOLD  2341  pm11.53  2344  19.12vv  2345  cbval2  2411  nfsb4t  2503  mof  2563  euf  2576  2eu3  2655  axextmo  2713  nfnfc1  2910  nfnfc  2919  nfabdwOLD  2931  sbcnestgfw  4352  sbcnestgf  4357  nfdisjw  5051  nfdisj  5052  nfdisj1  5053  axrep1  5210  axrep2  5212  axrep3  5213  axrep4  5214  nffr  5563  zfcndrep  10370  zfcndinf  10374  mreexexd  17357  mptelee  27263  mo5f  30837  iinabrex  30908  19.12b  33777  bj-cbv2v  34980  ax11-pm2  35019  wl-sb8t  35707  wl-mo2tf  35726  wl-eutf  35728  wl-mo2t  35730  wl-mo3t  35731  wl-sb8eut  35732  mpobi123f  36320  pm11.57  42007  pm11.59  42009  ichnfimlem  44915  ichnfim  44916  nfsetrecs  46392