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

Theorem nfal 2323
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
StepHypRef Expression
1 nfal.1 . . . 4 𝑥𝜑
21nf5ri 2195 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 2167 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nf5i 2146 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1538  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784
This theorem is referenced by:  nfex  2324  nfnf  2326  nfsbvOLD  2331  aaanOLD  2334  cbval2v  2345  pm11.53  2348  19.12vv  2349  cbval2  2416  nfsb4t  2504  mof  2563  euf  2576  2eu3  2654  axextmo  2712  nfnfc1  2908  nfnfc  2918  sbcnestgfw  4421  sbcnestgf  4426  nfdisjw  5122  nfdisj  5123  nfdisj1  5124  axrep1  5280  axrep2  5282  axrep3  5283  axrep4OLD  5286  nffr  5658  zfcndrep  10654  zfcndinf  10658  mreexexd  17691  mptelee  28910  mo5f  32508  iinabrex  32582  19.12b  35802  bj-cbv2v  36799  ax11-pm2  36837  wl-sb8t  37553  wl-mo2tf  37572  wl-eutf  37574  wl-mo2t  37576  wl-mo3t  37577  wl-sb8eut  37579  wl-sb8eutv  37580  mpobi123f  38169  pm11.57  44408  pm11.59  44410  ichnfimlem  47450  ichnfim  47451  nfsetrecs  49205  pgind  49236
  Copyright terms: Public domain W3C validator