Theorem nfal 2338

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

Syntax hints:  ∀wal 1531  Ⅎwnf 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-10 2141  ax-11 2157  ax-12 2173

This theorem depends on definitions:  df-bi 209  df-ex 1777  df-nf 1781

This theorem is referenced by:  nfex  2339  nfnf  2341  nfsbv  2345  nfsbvOLD  2346  aaan  2349  cbval2v  2359  cbval2vOLD  2360  pm11.53  2363  19.12vv  2364  cbval2  2428  cbval2OLD  2429  nfsb4t  2535  nfsb4tALT  2600  mof  2643  euf  2657  2eu3  2735  2eu3OLD  2736  axextmo  2797  nfnfc1  2980  nfnfc  2990  nfabdw  3000  sbcnestgfw  4369  sbcnestgf  4374  nfdisjw  5042  nfdisj  5043  nfdisj1  5044  axrep1  5190  axrep2  5192  axrep3  5193  axrep4  5194  nffr  5528  zfcndrep  10035  zfcndinf  10039  mreexexd  16918  mptelee  26680  mo5f  30252  19.12b  33046  bj-cbv2v  34120  ax11-pm2  34159  wl-sb8t  34787  wl-mo2tf  34806  wl-eutf  34808  wl-mo2t  34810  wl-mo3t  34811  wl-sb8eut  34812  mpobi123f  35439  pm11.57  40719  pm11.59  40721  dfich2OLD  43615  ichnfim  43623  nfsetrecs  44788