Theorem nfal 2327

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

Syntax hints:  ∀wal 1535  Ⅎwnf 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782

This theorem is referenced by:  nfex  2328  nfnf  2330  nfsbvOLD  2335  aaanOLD  2338  cbval2v  2349  pm11.53  2352  19.12vv  2353  cbval2  2419  nfsb4t  2507  mof  2566  euf  2579  2eu3  2657  axextmo  2715  nfnfc1  2911  nfnfc  2921  nfabdwOLD  2933  sbcnestgfw  4444  sbcnestgf  4449  nfdisjw  5145  nfdisj  5146  nfdisj1  5147  axrep1  5304  axrep2  5306  axrep3  5307  axrep4  5308  nffr  5673  zfcndrep  10683  zfcndinf  10687  mreexexd  17706  mptelee  28928  mo5f  32517  iinabrex  32591  19.12b  35765  bj-cbv2v  36764  ax11-pm2  36802  wl-sb8t  37506  wl-mo2tf  37525  wl-eutf  37527  wl-mo2t  37529  wl-mo3t  37530  wl-sb8eut  37532  wl-sb8eutv  37533  mpobi123f  38122  pm11.57  44358  pm11.59  44360  ichnfimlem  47337  ichnfim  47338  nfsetrecs  48778  pgind  48809