Theorem nfal 2317

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

Syntax hints:  ∀wal 1540  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138  ax-11 2155  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfex  2318  nfnf  2320  nfsbvOLD  2325  aaanOLD  2329  cbval2v  2340  pm11.53  2343  19.12vv  2344  cbval2  2411  nfsb4t  2499  mof  2558  euf  2571  2eu3  2650  axextmo  2708  nfnfc1  2907  nfnfc  2916  nfabdwOLD  2928  sbcnestgfw  4417  sbcnestgf  4422  nfdisjw  5124  nfdisj  5125  nfdisj1  5126  axrep1  5285  axrep2  5287  axrep3  5288  axrep4  5289  nffr  5649  zfcndrep  10605  zfcndinf  10609  mreexexd  17588  mptelee  28133  mo5f  31707  iinabrex  31778  19.12b  34711  bj-cbv2v  35614  ax11-pm2  35652  wl-sb8t  36355  wl-mo2tf  36374  wl-eutf  36376  wl-mo2t  36378  wl-mo3t  36379  wl-sb8eut  36380  mpobi123f  36968  pm11.57  43081  pm11.59  43083  ichnfimlem  46066  ichnfim  46067  nfsetrecs  47633  pgind  47664