MPE Home 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 2231 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 2204 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nf5i 2191 1 𝑥𝑦𝜑
Colors of variables: wff setvar class
Syntax hints:  wal 1635  wnf 1863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-10 2186  ax-11 2202  ax-12 2215
This theorem depends on definitions:  df-bi 198  df-ex 1860  df-nf 1864
This theorem is referenced by:  nfex  2332  nfnf  2336  nfaldOLD  2342  nfa2OLD  2344  aaan  2345  cbv3v  2347  pm11.53  2355  19.12vv  2356  cbv3  2440  cbval2  2452  nfsb4t  2550  euf  2647  mo2  2648  2eu3  2726  axextmo  2796  bm1.1OLD  2797  nfnfc1  2958  nfnfc  2965  nfnfcALT  2966  sbcnestgf  4199  nfdisj  4831  nfdisj1  4832  axrep1  4972  axrep2  4974  axrep3  4975  axrep4  4976  nffr  5292  zfcndrep  9724  zfcndinf  9728  mreexexd  16516  mptelee  25995  mo5f  29658  19.12b  32032  bj-cbv2v  33051  bj-cbval2v  33056  bj-axrep1  33104  bj-axrep2  33105  bj-axrep3  33106  bj-axrep4  33107  ax11-pm2  33138  wl-sb8t  33650  wl-mo2tf  33669  wl-eutf  33671  wl-mo2t  33673  wl-mo3t  33674  wl-sb8eut  33675  mpt2bi123f  34283  pm11.57  39090  pm11.59  39092  nfsetrecs  43002
  Copyright terms: Public domain W3C validator