Theorem nfal 2307

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

Syntax hints:  ∀wal 1523  Ⅎwnf 1769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-10 2114  ax-11 2128  ax-12 2143

This theorem depends on definitions:  df-bi 208  df-ex 1766  df-nf 1770

This theorem is referenced by:  nfex  2308  nfnf  2310  nfsbv  2314  nfsbvOLD  2315  aaan  2317  pm11.53  2325  19.12vv  2326  2sb8evOLD  2334  cbval2  2390  cbval2OLD  2391  nfsb4t  2495  nfsb4tALT  2560  mof  2605  euf  2623  2eu3  2711  2eu3OLD  2712  axextmo  2775  nfnfc1  2954  nfnfc  2961  sbcnestgf  4296  nfdisj  4948  nfdisj1  4949  axrep1  5089  axrep2  5091  axrep3  5092  axrep4  5093  nffr  5424  zfcndrep  9889  zfcndinf  9893  mreexexd  16752  mptelee  26368  mo5f  29941  19.12b  32657  bj-cbv2v  33671  bj-cbval2v  33674  ax11-pm2  33735  wl-sb8t  34340  wl-mo2tf  34359  wl-eutf  34361  wl-mo2t  34363  wl-mo3t  34364  wl-sb8eut  34365  mpobi123f  34993  pm11.57  40280  pm11.59  40282  dfich2OLD  43120  ichnfim  43128  nfsetrecs  44291