Theorem nfal 2336

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

Syntax hints:  ∀wal 1529  Ⅎwnf 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-10 2139  ax-11 2154  ax-12 2170

This theorem depends on definitions:  df-bi 209  df-ex 1775  df-nf 1779

This theorem is referenced by:  nfex  2337  nfnf  2339  nfsbv  2343  nfsbvOLD  2344  aaan  2347  cbval2v  2357  cbval2vOLD  2358  pm11.53  2361  19.12vv  2362  cbval2  2426  cbval2OLD  2427  nfsb4t  2533  nfsb4tALT  2598  mof  2641  euf  2655  2eu3  2733  2eu3OLD  2734  axextmo  2795  nfnfc1  2978  nfnfc  2988  nfabdw  2998  sbcnestgfw  4368  sbcnestgf  4373  nfdisjw  5034  nfdisj  5035  nfdisj1  5036  axrep1  5182  axrep2  5184  axrep3  5185  axrep4  5186  nffr  5522  zfcndrep  10028  zfcndinf  10032  mreexexd  16911  mptelee  26673  mo5f  30245  19.12b  33039  bj-cbv2v  34113  ax11-pm2  34152  wl-sb8t  34780  wl-mo2tf  34799  wl-eutf  34801  wl-mo2t  34803  wl-mo3t  34804  wl-sb8eut  34805  mpobi123f  35432  pm11.57  40711  pm11.59  40713  dfich2OLD  43606  ichnfim  43614  nfsetrecs  44779