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

Syntax hints:  ∀wal 1568  Ⅎwnf 1813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-10 2176  ax-11 2192  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814

This theorem is referenced 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  4386  sbcnestgf  4391  nfdisjw  5088  nfdisj  5089  nfdisj1  5090  axrep1  5239  axrep2  5241  axrep3  5242  axrep4OLD  5245  nffr  5634  zfcndrep  10594  zfcndinf  10598  mreexexd  17699  mpteleeOLD  29245  mo5f  32835  iinabrex  32914  axpowg3  35561  19.12b  36291  regsfromsetind  37070  bj-cbv2v  37453  ax11-pm2  37491  bj-axreprepsep  37732  wl-sb8t  38227  wl-mo2tf  38246  wl-eutf  38248  wl-mo2t  38250  wl-mo3t  38251  wl-sb8eut  38253  wl-sb8eutv  38254  mpobi123f  38831  pm11.57  45119  pm11.59  45121  permaxrep  45735  ichnfimlem  48232  ichnfim  48233  nfsetrecs  50484  pgind  50515  nfals  50601  nfalseu  50632