Theorem nfal 2357

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

This proof depends on syntax axioms:  ∀wal 1568  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-10 2180  ax-11 2197  ax-12 2216

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  nfex  2358  nfnf  2360  cbval2v  2376  pm11.53  2379  19.12vv  2380  cbval2  2443  nfsb4t  2531  mof  2591  euf  2604  2eu3  2681  axextmo  2739  nfnfc1  2929  nfnfc  2938  sbcnestgfw  4382  sbcnestgf  4387  nfdisjw  5087  nfdisj  5088  nfdisj1  5089  axrep1  5239  axrep2  5241  axrep3  5242  nffr  5631  zfcndrep  10738  zfcndinf  10742  mreexexd  17872  mpteleeOLD  29530  mo5f  33184  iinabrex  33261  axpowg3  35957  srepdf  36128  19.12b  36778  regsfromsetind  37542  bj-cbv2v  37925  ax11-pm2  37963  bj-axreprepsep  38261  wl-sb8t  38752  wl-mo2tf  38771  wl-eutf  38773  wl-mo2t  38775  wl-mo3t  38776  wl-sb8eut  38778  wl-sb8eutv  38779  mpobi123f  39360  pm11.57  45634  pm11.59  45636  permaxrep  46260  ichnfimlem  48818  ichnfim  48819  nfsetrecs  51195  pgind  51216  nfals  51327  nfalseu  51358