Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfal Structured version   Visualization version   GIF version

Theorem nfal 2331
 Description: If 𝑥 is not free in 𝜑, 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
StepHypRef Expression
1 nfal.1 . . . 4 𝑥𝜑
21nf5ri 2193 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 2171 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nf5i 2147 1 𝑥𝑦𝜑
 Colors of variables: wff setvar class Syntax hints:  ∀wal 1536  Ⅎwnf 1785 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-11 2158  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786 This theorem is referenced by:  nfex  2332  nfnf  2334  nfsbv  2338  nfsbvOLD  2339  aaan  2342  cbval2v  2352  cbval2vOLD  2353  pm11.53  2356  19.12vv  2357  cbval2  2421  cbval2OLD  2422  nfsb4t  2517  nfsb4tALT  2580  mof  2622  euf  2636  2eu3  2715  axextmo  2774  nfnfc1  2958  nfnfc  2967  nfabdw  2976  sbcnestgfw  4326  sbcnestgf  4331  nfdisjw  5007  nfdisj  5008  nfdisj1  5009  axrep1  5155  axrep2  5157  axrep3  5158  axrep4  5159  nffr  5493  zfcndrep  10027  zfcndinf  10031  mreexexd  16913  mptelee  26696  mo5f  30267  iinabrex  30339  19.12b  33171  bj-cbv2v  34251  ax11-pm2  34290  wl-sb8t  34969  wl-mo2tf  34988  wl-eutf  34990  wl-mo2t  34992  wl-mo3t  34993  wl-sb8eut  34994  mpobi123f  35616  pm11.57  41108  pm11.59  41110  ichnfimlem  43995  ichnfim  43996  nfsetrecs  45230
 Copyright terms: Public domain W3C validator