Theorem nfal 2314

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

Syntax hints:  ∀wal 1537  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-10 2135  ax-11 2152  ax-12 2169

This theorem depends on definitions:  df-bi 206  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfex  2315  nfnf  2317  nfsbvOLD  2322  aaanOLD  2326  cbval2v  2337  pm11.53  2340  19.12vv  2341  cbval2  2408  nfsb4t  2496  mof  2555  euf  2568  2eu3  2647  axextmo  2705  nfnfc1  2904  nfnfc  2913  nfabdwOLD  2925  sbcnestgfw  4419  sbcnestgf  4424  nfdisjw  5126  nfdisj  5127  nfdisj1  5128  axrep1  5287  axrep2  5289  axrep3  5290  axrep4  5291  nffr  5651  zfcndrep  10613  zfcndinf  10617  mreexexd  17598  mptelee  28418  mo5f  31994  iinabrex  32065  19.12b  35075  bj-cbv2v  35981  ax11-pm2  36019  wl-sb8t  36722  wl-mo2tf  36741  wl-eutf  36743  wl-mo2t  36745  wl-mo3t  36746  wl-sb8eut  36747  mpobi123f  37335  pm11.57  43452  pm11.59  43454  ichnfimlem  46431  ichnfim  46432  nfsetrecs  47820  pgind  47851