Theorem nfal 2356

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

This proof depends on syntax axioms:  ∀wal 1567  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-10 2179  ax-11 2196  ax-12 2215

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

This theorem is used by:  nfex  2357  nfnf  2359  cbval2v  2375  pm11.53  2378  19.12vv  2379  cbval2  2443  nfsb4t  2531  mof  2591  euf  2604  2eu3  2681  axextmo  2739  nfnfc1  2928  nfnfc  2937  sbcnestgfw  4381  sbcnestgf  4386  nfdisjw  5084  nfdisj  5085  nfdisj1  5086  axrep1  5235  axrep2  5237  axrep3  5238  nffr  5627  zfcndrep  10709  zfcndinf  10713  mreexexd  17834  mpteleeOLD  29485  mo5f  33139  iinabrex  33217  axpowg3  35887  srepdf  36041  19.12b  36690  regsfromsetind  37454  bj-cbv2v  37837  ax11-pm2  37875  bj-axreprepsep  38130  wl-sb8t  38624  wl-mo2tf  38643  wl-eutf  38645  wl-mo2t  38647  wl-mo3t  38648  wl-sb8eut  38650  wl-sb8eutv  38651  mpobi123f  39234  pm11.57  45513  pm11.59  45515  permaxrep  46135  ichnfimlem  48684  ichnfim  48685  nfsetrecs  51003  pgind  51024  nfals  51113  nfalseu  51144